一句话：提出 LOUD 框架，为含存在量词的非确定程序同时合成最强 ℒ-推论与最弱 ℒ-蕴含式规范。
本文研究非确定程序的规范合成问题。此类程序既有对所有非确定执行成立的 demonic 性质，也有对某些执行成立的 angelic 性质。现有 spyro 框架只能处理无量词查询并合成最强的 ℒ-推论（过近似），无法表达非确定性和 angelic 性质。作者提出 LOUD 框架，支持带存在量词的查询，并同时合成最强 ℒ-推论与最弱 ℒ-蕴含式（欠近似）。文中给出处理查询中量词的算法，并实现求解器 ASPIRE。该求解器可用于定位确定/非确定程序中的缺陷、从并发程序中抽取性质，以及合成双人博弈的获胜策略。
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 spyro framework 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 ℒ in which each extracted property is to be expressed (we call properties in the language ℒ-properties), the goal is to synthesize a conjunction ∧ 𝑖 𝜑 𝑖 of ℒ-properties such that each of the 𝜑 𝑖 is a strongest ℒ -consequence for Ψ: 𝜑 𝑖 is an overapproximation of Ψ and there is no other ℒ-property that over-approximates Ψ and is strictly more precise than 𝜑 𝑖 . 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 ℒ-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 ℒ -consequences and weakest ℒ -implicants (i.e., under-approximations of the query Ψ) for queries that can involve existential quantifiers . We devise algorithms for handling the quantifiers appearing in loud queries and implement them in 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.
@article{paperbot3214,
title = {LOUD: Synthesizing Strongest and Weakest Specifications},
author = {Kanghee Park and Xuanyu Peng and Loris D'Antoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720470}
}