Abstract
Specifications allow us to formally state and understand what programs are intended to do. To help one extract useful properties from code, Park et al. recently proposed a framework that given (i) a quantifier-free query posed about a set of function definitions, and (ii) a domain-specific language L in which each extracted property is to be expressed (we call properties in the language L-properties), synthesizes a set of L-properties such that each of the property is a strongest L-consequence for the query: the property is an over-approximation of query and there is no other L-property that over-approximates query and is strictly more precise than each property. The framework by Park et al. has two key limitations. First, it only supports quantifier-free query formulas and thus cannot synthesize specifications for queries involving nondeterminism, concurrency, etc. Second, it can only compute L-consequences, i.e., over-approximations of the program behavior. This paper addresses these two limitations and presents a framework, Loud, for synthesizing strongest L-consequences and weakest L-implicants (i.e., under-approximations of the query) for function definitions that can involve existential quantifiers. We implemented a solver, Aspire, for problems expressed in Loud which can be used to describe and identify sources of bugs in both deterministic and nondeterministic programs, extract properties from concurrent programs, and synthesize winning strategies in two-player games.
Type
Publication
Object-Oriented Programming, Systems, Languages & Applications 2025
This work extends the specification-synthesis framework from my previous paper to a more general setting. The earlier framework synthesized strongest properties for quantifier-free queries; LOUD handles queries with existential quantifiers and supports both over-approximating and under-approximating specifications.
This matters for programs with nondeterministic or concurrent behavior, where useful specifications can describe what must happen across all executions as well as what can happen along some execution. LOUD captures these two views through strongest L-consequences and weakest L-implicants.
The paper introduces the LOUD framework and the ASPIRE solver. The evaluation uses the framework to describe and localize bugs, extract properties from concurrent programs, and synthesize winning strategies in two-player games.
