LOUD: Synthesizing Strongest and Weakest Specifications

TL;DR

LOUD extends specification synthesis to nondeterministic programs by enabling existential quantifiers and both angelic and demonic reasoning. It introduces ASPIRE, a solver built on Sketch that pairs counterexample-guided synthesis with counterexample-guided quantifier instantiation (CEGQI/CEGIS) to compute strongest $\mathcal{L}$-consequences and weakest $\mathcal{L}$-implicants, respectively. The framework supports over- and under-approximations, enabling applications in incorrectness reasoning, concurrent programming, and two-player games, among others. This unified approach enables targeted extraction of bug sources, invariants, and winning strategies, with practical evaluation across diverse domains. Limitations include reliance on bounded inputs from Sketch and potential scalability constraints, motivating future integration with verifiers for unbounded or reactive settings.

Abstract

This paper tackles the problem of synthesizing specifications for nondeterministic programs. For such programs, useful specifications can capture demonic properties, which hold for every nondeterministic execution, but also angelic properties, which hold for some nondeterministic execution. We build on top of a recently proposed a framework by Park et al. in which given (i) a quantifier-free query posed about a set of function definitions (i.e., the behavior for which we want to generate a specification), and (ii) a language L in which each extracted property is to be expressed (we call properties in the language L-properties), the goal is to synthesize a conjunction of L-properties such that each of the conjunct is a strongest L-consequence for the query: each property is an over-approximation of the query and there is no other L-property that over-approximates the query and is strictly more precise than each property. This framework does not apply to nondeterministic programs for two reasons: it does not support existential quantifiers in queries (which are necessary to expressing nondeterminism) and it can only compute L-consequences, i.e., it is unsuitable for capturing both angelic and demonic properties. This paper addresses these two limitations and presents a framework, LOUD, for synthesizing both strongest L-consequences and weakest L-implicants (i.e., under-approximations of the query) for queries that can involve existential quantifiers. We implement 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.

Figures (13)

• Figure 1: (a) A query $\Psi$ for identifying properties of modhash that hold for any choice of input $\textcolor{dblue}{x}$. Users declare variables and label existentially quantified ones with the keyword exist. (b) A DSL $\mathcal{O}$ for over-approximations. \\/[AP, 0..6] is a shorthand for the disjunction of 0 to 6 atomic propositions. (c) $\mathcal{O}$-consequences by our tool aspire when given the query $\Psi$ and the DSL $\mathcal{O}$. We write $p \Rightarrow q$ instead of $\neg p \vee q$ for readability.
• Figure 2: modhash function
• Figure 3: Synthesized $\mathcal{U}$-implicants.
• Figure 4: The bounded domains of variables in problem \ref{['se:example-reachability-over']}
• Figure 5: remhash function

Theorems & Definitions (29)

• Definition 3.1: A strongest $\mathcal{L}$-consequence
• Definition 3.2: A weakest $\mathcal{L}$-implicant
• Definition 3.3: Best $\mathcal{L}$-conjunction
• Definition 3.4: Best $\mathcal{L}$-disjunction
• theorem 1: Semantic Optimality
• Definition 3.5: Best $\mathcal{L}$-conjunction and $\mathcal{L}$-disjunction Synthesis
• Definition 4.1: Examples
• Example 4.1: Positive and Negative Examples
• Example 4.2: Examples and $\mathcal{L}$-consequences
• Example 4.3: Examples and $\mathcal{L}$-implicants