# LOUD: Synthesizing Strongest and Weakest Specifications

Kanghee Park,
Xuanyu Peng,
Loris D'Antoni

July, 2024

### 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 $\Psi$ posed about a set of function definitions, and (ii) a domain-specific language $\mathcal{L}$ in which each extracted property is to be expressed (we call properties in the language $\mathcal{L}$-properties), synthesizes a set ${\varphi_1, \ldots , \varphi_n}$ of $\mathcal{L}$-properties such that each of the $\varphi_i$ is a **strongest $\mathcal{L}$-consequence** for $\Psi$, i.e., $\varphi_i$ is an over-approximation of $\Psi$ and there is no other $\mathcal{L}$-property that over-approximates $\Psi$ and is strictly more precise than $\varphi_i$.

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 $\mathcal{L}$-consequences, i.e., **over-approximations** of the program behavior.

This paper addresses these two limitations and presents a framework, Loud, for synthesizing strongest $\mathcal{L}$-consequences and **weakest $\mathcal{L}$-implicants** (i.e., under-approximations of the query $\Psi$) 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.

Click the *Cite* button above to demo the feature to enable visitors to import publication metadata into their reference management software.

Create your slides in Markdown - click the *Slides* button to check out the example.

Supplementary notes can be added here, including code, math, and images.

I’m DOFY, a PhD student in computer science at UCSD