SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications
Nanjing University（南京大学）
针对现有LLM规范综合方法在复杂程序上易失效的问题，提出SpecAgent智能体框架，通过依赖感知规划、RAG、智能体修复与评判，在真实C程序上实现96.82%精确率与88.95%召回率，并成功解决604个验证目标。
2026-10-06 cs.SE
Efficient Reactive Synthesis Using Mode Decomposition
针对LTL反应式综合计算复杂度高、难以适配大规模场景的问题，提出基于模式的新型分解算法，将复杂安全规约分解为子问题后顺序组合解，证明了方法的正确性并通过案例验证了可行性。
2023-12-14 cs.LO cs.SE
Towards a Pattern-based Automatic Generation of Logical Specifications for Software Models
这项工作涉及到自动生成的逻辑规范，被认为是一套时间逻辑公式，直接从开发的软件模型中提取。提取过程是基于这样的假设，即整个开发模型的结构只使用预定义的工作流模式。提出了一种工作流模式到逻辑规范的自动转换方法。应用所提出的概念，使弥合之间的差距的正确性验证过程中获得完整的逻辑规范的困难和演绎推理的好处。
2014-06-26 cs.SE
Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis
本研究提出结合大型语言模型Deepseek-R1与Frama-C符号分析工具，从C代码生成ACSL形式化规约，探讨了意图与实现规约的差异及符号分析对规约质量的提升。
2025-04-29 cs.SE
Structural Synthesis for GXW Specifications
我们定义的GXW片段的线性时序逻辑（LTL）的基础上合成嵌入式控制软件的安全关键型应用程序。由于GXW包括使用弱直到操作符，我们能够指定一些不同的可编程逻辑控制（PLC）的问题，我们已经从工业训练集编译。对于GXW控制器规范，我们开发了一种新的方法来合成一组同步通信的基于演员的控制器。该综合算法通过对GXW规范的结构进行递归，并根据公式结构生成一组专用的同步通信子控制器。在后续步骤中，2QBF约束求解识别并尝试解决各个GXW规范之间的潜在冲突。GXW合成的这种结构化方法支持安全关键软件认证制度所要求的需求和生成的控制代码之间的可追溯性。GXW规范的合成是在PSPACE中进行的，而2EXPTIME是完整的LTL合成。事实上，我们的实验结果表明，GXW合成规模以及工业规模的控制合成问题，20个输入和输出端口及以上。
2016-07-06 cs.LO cs.SE
Learning to adapt GR(1) specifications through degradation
Imperial College London（帝国理工学院）；Universidad de Buenos Aires（布宜诺斯艾利斯大学）；CONICET（阿根廷国家科学与技术研究理事会）；Universidad de San Andrés（圣安德烈斯大学）
针对GR(1)规范在环境假设违反时系统保证失效的问题，提出基于预言引导归纳综合的规范调整方法，通过最小化降级系统保证以维持可实现性，并在案例中保留全部原始保证。
2026-09-14 cs.AI cs.LO cs.SE
Reactive Synthesis from Extended Bounded Response LTL Specifications
反应合成是一个关键技术的设计正确的建设系统，并已在过去的几十年里进行了深入的研究。它包括在一个控制器的合成，反应环境的输入满足给定的时序逻辑规范。常见的方法是基于自动机的显式构造和它们的确定性，这限制了它们的可扩展性。在本文中，我们引入了一个新的片段的线性时序逻辑，称为扩展有界响应LTL（\LTLEBR），它允许一个结合有界和普遍无界的时间运营商（从而涵盖了大量的实际情况），我们表明，反应合成从\LTLEBR规范可以减少到解决一个安全游戏的确定性的符号自动机直接从规范。我们证明了所提出的方法的正确性，我们成功地评估它在各种基准。
2020-08-12 cs.FL cs.LO cs.SE
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
反应系统的自动综合规范已经研究了几十年的主题。近年来，人们提出了多种方法，将反应系统的综合从建议性规范扩展到丰富理论的规范。我们提出了一种新的，完全自动化的方法来程序合成，减少了问题，以决定一组forall存在的公式的有效性。在IC3/PDR的精神，我们的问题空间是递归细化，通过封锁不安全状态的区域，旨在发现一个不动点，描述安全的反应。如果找到了这样的不动点，我们就构造一个直接转换为实现的见证。我们在JKind模型检查器之上实现了该算法，并对使用Lustre规约语言编写的契约进行了测试。实验结果表明，新算法如何优于JKinds已经存在的合成过程的基础上k-归纳和解决健全的问题，在k-归纳的方法相对于无法实现的结果。
2018-03-21 cs.SE
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
Chalmers University of Technology（查尔姆斯理工大学）
本研究结合大语言模型与Frama-C生态的Pathcrawler、EVA符号分析工具，增强ACSL格式C程序规约合成质量，且方法更倾向推断程序意图而非实际行为。
2024-09-18 cs.FL cs.LG cs.SE
Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
本文提出 AutoSpec 方法，结合静态分析、程序验证与大型语言模型，通过程序分解和逐轮验证迭代生成满足性且充分的程序规约，成功验证 79% 的程序，显著优于现有工作。
2024-04-02 cs.SE
SpecFirst: Behavioral Specification Elicitation as a First-Class Step in Agent-Based Program Synthesis from Scratch
Queen's University（女王大学）；University of Manitoba（曼尼托巴大学）；Concordia University（康考迪亚大学）
SpecFirst是将行为规范提取设为独立前置阶段的两阶段框架，在ProgramBench上显著提升了从零开始的程序合成的测试通过率与二进制探索覆盖率。
2026-07-30 cs.CL cs.SE
Maximum Realizability for Linear Temporal Logic Specifications
基于线性时序逻辑（LTL）规范的自动综合广泛应用于机器人运动规划、自治系统控制和电网负荷分配等领域。在这样的应用程序中，一个常见的规范模式包括一个LTL公式，描述了对系统的行为的要求，以及一组额外的理想属性。我们研究的综合问题的整体规格是无法实现的设置，更准确地说，当一些理想的属性必须（暂时）违反，以满足系统的目标。我们提供了一个定量的语义集的安全规范，并使用它来正式的“尽力而为”的满足这样的软规范，同时满足硬LTL规范。我们提出了一种算法，用于合成的实现，是最佳的定量语义。我们的方法建立在有界合成方法的思想，我们开发了一个MaxSAT编码，允许最大限度地满足安全规范的定量。我们评估我们的算法从机器人和配电网络的情况。
2018-04-02 cs.LO cs.SE
Exploring the Link Between Test Suite Quality and Automatic Specification Inference
虽然没有人怀疑正确和完整的规范的重要性，但许多工业系统仍然没有正式的规范-即使他们这样做了，也很难检查其正确性和完整性。这项工作探讨了使用一个不变的提取工具，如Daikon自动推断规格，从可用的测试套件的想法，帮助软件工程师，以改善规范，有另一个版本进行比较的可能性。鉴于我们最初的实验并没有产生令人满意的结果，在本文中，我们将探讨哪些测试套件属性影响质量的推断规范。进一步研究发现，指令、分支和方法覆盖率与高召回率相关，最高可达97.93%。
2017-08-24 cs.LO cs.SE
Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications
针对从轻量级规范合成同步分布式模型的问题，提出一种基于Alloy Analyzer编码组件规范并枚举有界实现、通过多批反例修剪解空间加速搜索的方法，输出满足全局约束的Promela风格可执行模型，还展示了原型工具并进行了实验对比。
2025-02-19 cs.SE
SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
Nanjing University（南京大学）；Nanyang Technological University（南洋理工大学）
本文提出SpecSyn，一种基于大语言模型的规范生成方法，通过分解程序并引入语义非等价变异和变体辨别机制，提升规范的语义强度，实验显示其在精度和召回率上显著优于现有方法。
2026-10-11 cs.SE
Agentic Separation Logic Specification Synthesis
Bloomberg（贝莱德）
提出 Spec-Agent 智能体系统，通过静态分析、运行时堆追踪和反例引导迭代，为大型 C++ 代码库合成分离逻辑规范，在百万行级代码上达到 85% 有效规范合成率且无假阳性。
2026-05-26 cs.CL cs.PL cs.SE
A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
Zhejiang University（浙江大学）；Peking University（北京大学）；The Chinese University of Hong Kong（香港中文大学）；Xidian University（西安电子科技大学）；Beijing Institute of Control Engineering（北京控制工程研究所）
Preguss通过结合静态分析与演绎验证，实现大规模程序的自动化形式化验证，显著提升验证效率。
2026-03-10 cs.LO cs.SE
Synthesizing a Lego Forklift Controller in GR(1): A Case Study
反应合成是从给定的规格获得正确的结构反应体系的自动化过程。GR（1）是线性时序逻辑（LTL）的一个众所周知的片段，其中可以使用多项式符号算法进行合成。我们进行了一个案例研究，以了解软件工程师在使用GR（1）合成开发反应式机器人系统时可能面临的挑战。在案例研究中，我们开发了叉车控制器的两个变体，部署在乐高机器人上。案例研究采用LTL规范模式作为GR（1）规约语言的扩展，检查执行调度的两个规范变量，从合成控制器到规范中的约束的可追溯性，并生成计数器策略以支持理解不可实现的原因。我们提出了我们开发的规范，我们的意见，并在案例研究中面临的挑战。
2016-02-03 cs.SE
Model Based Synthesis of Control Software from System Level Formal Specifications
Sapienza University of Rome（罗马大学）
提出一种算法及工具QKS，从被控系统的形式化模型、实现规范和系统级形式化规范自动综合出满足安全性和活性要求且最坏情况执行时间与AD位数线性相关的控制软件。
2013-04-27 cs.SE cs.SY eess.SY
Unrealizable Cores for Reactive Systems Specifications
反应合成是一种自动化的过程，以获得正确的结构反应体系，其主要挑战之一是处理不可实现的规格。在GR（1）的上下文中，处理不可实现性的一种方法是计算不可实现的核心，这可以被视为一种故障定位方法，GR（1）是LTL的一个表达性的假设保证片段，可以实现有效的合成。然而，现有的解决方案在计算上是昂贵的，仅限于计算单个核心，并且不能正确地支持具有超越纯GR（1）元素的构造的规范。在这项工作中，我们解决这些限制。首先，我们提出了QuickCore，一种新的算法，它通过依赖于不可实现性的单调性，增量计算和GR（1）规范的附加属性来加速不可实现的核心计算。其次，我们提出了打孔，一种新的算法，有效地计算所有无法实现的核心的规范。最后，我们提出了正确处理规范的方法，这些规范包括纯GR（1）元素之外的更高级别的构造。我们在Spectra之上实现了我们的想法，Spectra是一个开放的源语言和合成环境。我们对文献中的基准测试的评估表明，QuickCore在大多数情况下比以前的算法更快，并且其相对优势随着规模的增长而增长。此外，我们发现大多数规范都包含多个核心，而Punch找到所有核心的速度明显快于竞争对手的朴素算法。
2021-02-27 cs.SE
ObSynth: An Interactive Synthesis System for Generating Object Models from Natural Language Specifications
Massachusetts Institute of Technology（麻省理工学院）
我们介绍ObSynth，一个交互式系统，利用嵌入在大语言模型（LLM）的领域知识，以帮助用户设计对象模型，从高层次的自然语言提示。这是规范具体化的一个例子，将一个高层次的、潜在的模糊规范具体化为一个更具体的形式。我们通过用户研究评估ObSynth，得出三个关键发现：首先，使用ObSynth设计的对象模型更详细，表明它经常合成用户可能忽略的字段。其次，ObSynth生成的大多数对象、方法和字段都由用户保存在最终的对象模型中，突出了生成组件的质量。第三，ObSynth改变了参与者的工作流程：他们专注于检查合成组件是否正确，而不是从头开始生成它们，尽管ObSynth并没有减少参与者生成对象模型的时间。
2022-10-20 cs.HC cs.LG cs.SE
Operads for complex system design specification, analysis and synthesis
随着系统复杂性和异构性的增长，指定、记录和合成正确的机器可读设计的挑战也急剧增加。需要将系统分离为可管理的部分，以支持不同粒度级别的分析，从而使系统在其生存周期内可维护和自适应。在本文中，我们认为，操作提供了一个有效的知识表示，以解决这些挑战。在设计综合过程中，通过对设计有效性的语义推理，建立了语法正确的设计的正式文档。在整个过程中，保持将系统分解为部分并重构整体的能力。我们描述了最近的进展，在这种模式下，有效的建模和未来的工作方向，系统地解决复杂系统设计的可扩展性的挑战。
2021-05-25 cs.SE math.CT
ARSENAL: Automatic Requirements Specification Extraction from Natural Language
SRI International（SRI国际公司）；TTTech C. AG（TTTech股份公司）
需求是从利益相关者（客户、用户、操作员、设计师和工程师）的角度对复杂系统预期行为的非正式和半正式描述。然而，对于关键系统的设计、测试和验证，我们可以将需求转换为可以自动分析的形式化模型。ARSENAL是一个框架和方法，用于系统地将自然语言（NL）需求转换为可分析的形式化模型和逻辑规范。可以分析这些模型的一致性和可实现性。ARSENAL方法专门针对各个领域，但该方法足够通用，可以适应新的领域。
2016-04-20 cs.CL cs.SE
Low-Effort Specification Debugging and Analysis
University of Bremen（不来梅大学）；DFKI GmbH（德国人工智能研究中心有限公司）；California Institute of Technology（加州理工学院）
反应式合成处理从其规范自动构建反应式系统的实现。为了使这种方法在实践中可行，系统工程师需要有效和高效的手段来调试这些规范。在本文中，我们提供了基于报告的规范调试技术，其中一个规范的显着属性进行了分析，并将结果以报告的形式呈现给用户。这提供了一种低工作量的调试规范的方法，补充了高工作量的技术，包括模拟合成的实现。我们证明了我们的报告为基础的规范调试工具包的有用性，通过提供的情况下，广义反应性（1）合成的例子。
2014-07-21 cs.LO cs.RO cs.SE
Automatic Verification of Parametric Specifications with Complex Topologies
本文的重点是降低验证的复杂性，利用模块化在各个层次上：在规范，验证，和结构。对于规范，我们使用的模块化语言CSP-OZ-DC，它允许我们解耦验证任务有关的数据从那些有关的持续时间。在验证级别，我们利用模块化的定理证明丰富的数据结构，并使用此不变检查。在结构层面上，我们分析了模块化验证的系统组成的各种组件的相互作用的可能性，我们说明了这些想法，通过自动验证安全性能的案例研究，从欧洲训练控制系统标准，它扩展了以前的例子，包括一个复杂的轨道拓扑结构与列表的轨道段和列车与不同的路线。
2010-10-08 cs.LO cs.SE
Specification Mining for Smart Contracts with Automatic Abstraction Tuning
智能合约是根据特定协议管理数字资产的程序，例如表示拍卖规则。理解智能合约的可能行为是困难的，这使得开发、审计和攻击的事后分析变得复杂。本文介绍了智能合约的第一个规范挖掘技术。我们的技术从区块链上记录的合约执行中提取智能合约的可能行为，并将其表示为有限自动机。一种新的依赖分析允许我们将独立的交互与合同分开。例如，我们的技术根据可配置的指标自动调整自动机构造的抽象，以最大限度地提高可读性或精度。我们为以太坊区块链实现了我们的技术，并在几个现实世界的合同上评估了它的可用性。
2018-07-20 cs.PL cs.SE
Revisiting Timed Specification Theory II : Realisability
在本文中，我们提出了一个假设保证规格理论（又名接口理论[14]）的模块化综合和验证的实时系统的关键时间约束。这是我们早期工作的进一步发展[10]，该工作为具有冻结时间能力的实时系统实现了一个优雅的代数规范理论。在本文中，我们放弃这种（不可实现的）能力，并针对更现实的系统，而没有停止时间的能力。我们的理论，在一个组合的过程代数和反应式综合风格，提供了操作的并行组合系统集成，逻辑合取/析取的观点融合和独立发展，和商的增量综合。我们证明了一个替换加细预序，它是[10]中预同余的粗化，构成了最弱的预同余保持不相容错误的自由。粗化需要我们的理论的重点转移到一个更游戏理论的治疗，粗化构成了一个反应性的合成游戏命名为规范化，并有效地实现了一个新的本地机器人反向传播算法。以前，时间并发游戏已经在[1，14，13]中进行了研究，其中一个关键问题是通过应用责备分配来消除时间阻塞策略[13]。我们的定时游戏也有时间阻塞策略的问题，这可能会出现通过规范的组成。然而，由于我们对定时游戏的不同表述，我们发现了另一个优雅的解决方案，而没有责任分配。我们的解决方案利用了第二个反应性合成游戏称为实现，这是双重规范化和实现的双重本地顶部反向传播算法。
2013-04-29 cs.LO cs.SE
Towards Automatically Extracting UML Class Diagrams from Natural Language Specifications
在模型驱动工程（MDE）中，UML类图是开发人员之间进行计划和通信的一种方式。然而，它是复杂和消耗资源的。我们提出了一个自动化的方法提取UML类图从自然语言软件规格说明。为了开发我们的方法，我们在志愿者的帮助下创建了一个UML类图及其英文规范的数据集。我们的方法是一个管道的步骤组成的分割成句子的输入，句子的分类，从句子的UML类图片段的生成，并组成这些片段到一个UML类图。我们开发了一个定量测试框架，具体到UML类图提取。我们的方法产生低精度和召回率，但作为未来研究的基准。
2022-10-27 cs.IR cs.SE
Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
本文提出将 LLM 代码生成与基于形式化方法的反应式程序综合结合，通过分工处理复杂逻辑，并构建基准验证其可解决以往 LLM 难以完成的代码生成问题。
2024-09-18 cs.LG cs.LO cs.SE
