Toward Neural-Network-Guided Program Synthesis and Verification
The University of Tokyo（东京大学）；National Institute of Informatics（国立情报学研究所）；SOKENDAI（综合研究大学院大学）；University of Tsukuba（筑波大学）；RIKEN AIP（理化学研究所革新智能统合研究中心）
我们提出了一个新的框架的程序和不变量的合成称为神经网络指导合成。我们首先表明，通过适当的设计和训练神经网络，我们可以从训练好的神经网络的权重和偏差中提取整数上的逻辑公式。基于这一思想，我们实现了一个从正例/反例和蕴涵约束合成公式的工具，并获得了令人满意的实验结果。我们还讨论了我们的合成方法的两个应用。一个是使用我们的工具，限定符发现的框架ICE学习为基础的CHC解决，这反过来又可以应用于程序验证和归纳不变的合成。另一个应用是一个新的程序开发框架，称为基于甲骨文的编程，这是一个神经网络引导的变化Solar-Lezama的程序合成的草图。
2021-08-25 cs.LG cs.PL
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
这些会议记录包括在第九届验证和合成霍恩条款研讨会和第十届验证和程序转换国际研讨会上提交的选定论文，这两个研讨会都隶属于ETAPS 2022。许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。VPT研讨会的目的是汇集在程序验证和程序转换领域工作的研究人员。这两个领域之间有很大的潜力进行有益的互动，因为：1）一方面，在程序转换领域开发的方法和工具，如部分评估，折叠/展开转换和超级编译，都已成功应用于验证无限状态和参数化系统。2)另一方面，模型检验，抽象解释，SAT和SMT解决和自动定理证明已被用来加强程序转换技术。此外，程序转换工具的正式认证，如自动重构工具和编译器，最近吸引了相当大的兴趣，提出了重大挑战。
2022-11-19 cs.LO cs.PL cs.SC
Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
University of California, Berkeley（加州大学伯克利分校）
即使在自动化的形式化方法令人印象深刻的进步，在系统验证和综合的某些问题仍然具有挑战性。例子包括验证软件的定量属性，包括对时间和能量消耗的约束，以及从规范中自动合成系统。主要的挑战包括环境建模、规范的不完整性以及底层决策问题的复杂性。本文提出了一种通过整合归纳推理、演绎推理和结构假设来应对这些挑战的方法。演绎推理，从一般规则或概念导出关于特定问题实例的结论，包括逻辑推理和约束求解等技术。归纳推理，从特定的实例中概括出一个概念，包括从例子中学习算法。结构假设用于定义工件的类别，例如在验证或合成过程中生成的不变量或程序片段。演绎使用结构假设来约束归纳和演绎推理，并积极地结合归纳和演绎推理：例如，演绎技术生成用于学习的示例，并且归纳推理用于指导演绎引擎。我们用三个应用来说明这种方法：（i）软件的时序分析;（ii）无循环程序的合成，以及（iii）混合系统的控制器合成。一些未来的应用进行了讨论。
2012-01-04 cs.AI cs.LO cs.PL
Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
本文设计了首个 Unrealizability Logic (UL) 证明合成算法 Wuldo，通过解耦规则应用与非终结符摘要合成，实现了无限程序集合的可复用自动化验证，验证速度提升 1.96 倍。
2024-08-28 cs.PL
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification (Extended Version)
基于分布式协议（DAB）的系统使用常见的分布式协议协议，如领导者选举和共识作为其目标功能的构建块。虽然DAB系统的自动化验证是不可判定的一般，最近的工作确定了一个大类的DAB系统的验证是有效的可判定的。不幸的是，这种类别的特征条件可能是不透明和非直观的，并且可能对试图在此类中建模其系统的系统设计者构成重大挑战。在本文中，我们提出了一个合成驱动的工具，朱砂，以帮助系统设计人员建立DAB系统“适合”他们的预期设计成一个有效的可判定类。特别是，从设计师提供的初始草图开始，Cinnabar使用反例引导程序生成草图完成。核心技术依赖于一组相关反例的紧凑编码。我们证明朱砂的有效性，成功和有效地合成各种有趣的DAB系统的完成。
2023-01-14 cs.DC cs.PL
Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis
会议记录包括阿尔贝托的主题论文，随后由洛伦佐克莱门特（美国）撰写的6份邀请论文。华沙），阿兰芬克尔（美国。Paris-Saclay），John Gallagher（Roskilde U.和IMDEA软件研究所）等，尼尔·琼斯（美国）Copenhagen）等人，Michael Leuschel（Heinrich-Heine U.）和Maurizio Proietti（IASI-CNR）等人。这些邀请论文之后是VPT 2020上接受的4篇常规论文和HCVS 2020的论文，其中包括三篇投稿论文和一篇关于第三届约束Horn子句求解器竞赛的邀请论文。此外，Andrzej Skowron（U.华沙），索菲雷诺（EPO）和莫阿约翰逊（查尔默斯大学），包括在内。
2020-08-06 cs.LO cs.PL cs.SC
Towards Automated Verification of LLM-Synthesized C Programs
本文提出 \synver{} 框架，通过对 LLM 生成的 C 程序施加语法与语义偏置，并基于 Verified Software Toolchain 构建验证工具，实现程序合成与自动化验证。
2025-10-20 cs.PL
Noise-aware Verification and Synthesis of Quantum Programs
Institute of Science and Technology in Austria (ISTA)（奥地利科学与技术研究所）
本文针对真实有噪声硬件上的量子程序，开发噪声感知量子霍尔逻辑，实现特定硬件量子程序的有界验证与噪声最优无循环量子程序综合，经IBM Qiskit评估，发现经典概率分支是量子编程最优的必要条件。
2026-10-21 cs.FL cs.LO cs.PL
SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs
Zhejiang University（浙江大学）；Southeast University（东南大学）；MIT（麻省理工学院）；Weixin AI Lab（微信AI实验室）；Renmin University（中国人民大学）
SKILLFORGE 是将形式化代码合成分解为原子技能库并结合验证循环协调的框架，在自然语言转 Dafny 程序任务上性能优于现有方法。
2026-09-01 cs.CL cs.PL
PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
本文提出 PolyVer，一种利用抽象、组合推理和综合技术直接验证多语言软件系统的方法，通过连接模型检验器与特定语言验证器并自动生成前置/后置条件契约，结合 CEGAR 与 CEGIS 迭代验证系统级属性。
2025-10-12 cs.PL
Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
本卷为LSFA 2023与HCVS 2023的会后论文集，涵盖逻辑与语义框架、Horn子句验证与综合等主题。
2024-04-21 cs.LO cs.PL cs.SC
Model Repair Revamped: On the Automated Synthesis of Markov Chains
本文概述了两种方法|基于反例引导的抽象精化（CEGAR）和反例引导的归纳综合（CEGIS），分别应用于有限状态概率模型和程序的自动综合。我们的CEGAR方法迭代分区的设计空间从这个空间的抽象开始，并通过一个轻量级的验证结果分析细化。CEGIS技术利用关键子系统作为反例来修剪所有在该输入上行为不正确的程序。我们展示了这些综合技术的适用性，概率方案的草图，POMDPs的控制器合成，和软件产品线。
2021-05-27 cs.PL
Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
Stanford University（斯坦福大学）；Shanghai Jiao Tong University（上海交通大学）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Amherst College（阿默斯特学院）；Nanjing University（南京大学）
Quokka通过利用大语言模型生成有用的循环不变式，提升程序验证效率，其评价导向框架在多个模型家族中表现出色，优于现有基于LLM的验证器。
2026-08-11 cs.AI cs.CL cs.LG
Vectorization of Verilog Designs and its Effects on Verification and Synthesis
UFMG（米纳斯吉拉斯联邦大学）；Cadence（楷登电子）
本文探讨了Verilog设计的向量化技术，通过引入向量化器提升形式验证工具的效率，减少内存消耗，并在EDA工具中验证了其效果。
2026-03-17 cs.AR cs.PL
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
QEDCartographer结合监督与强化学习，利用证明分支结构实现无奖励搜索，在CoqGym基准上自动证明21.4%的定理，优于现有工具，证明强化学习可有效提升证明合成搜索机制。
2024-12-17 cs.LG cs.PL cs.SE
Towards establishing formal verification and inductive code synthesis in the PLC domain
如今，形式化方法被用于各种领域，用于程序的验证或用于从模型生成代码生成，以提高软件的质量并降低成本。然而，仍然有一些领域，其中正式的方法没有被广泛采用，尽管提供了大量的可能的好处。这是可编程逻辑控制器（PLC）领域的情况。本文的目的是评估PLC开发的背景下，形式化方法的潜力。为此，形式化方法的一般概念，首先介绍，然后转移到PLC领域，从而在工程为导向的描述的技术是基于PLC开发的共同概念。基于此描述，我们采访了具有不同经验的PLC专业人员，以了解他们对该主题的看法，并确定PLC领域中可能的用例。调查结果表明，该技术在PLC领域具有很高的潜力，无论是作为直接支持开发人员的工具，还是作为基于模型的系统工程工具链中的关键元素。调查结果的评估是在演示应用程序的帮助下进行的，该应用程序与西门子的全集成自动化门户进行通信，并通过基于模型的开源代码生成器Fastsynth生成程序。基于行业相关PLC项目的基准测试显示出令人满意的合成时间，并成功集成到PLC开发人员的工作流程中。
2021-06-30 cs.FL cs.PL cs.SE
Decidable Synthesis of Programs with Uninterpreted Functions
我们确定了一个可判定的合成问题的一类程序的无限大小的条件和迭代工作在无限的数据域。我们类中的程序使用未解释的函数和关系，并遵守最近确定的产生可判定验证的称为一致性的限制。我们制定了一个功能强大的语法限制（语法指导）的合成问题，连贯的未解释的程序，我们的问题是可判定的，确定其精确的复杂性，并研究了几个变种的问题。
2020-07-22 cs.FL cs.LO cs.PL
On Scaling Data-Driven Loop Invariant Inference
Microsoft Research, India（微软研究院（印度））；University of California Los Angeles, USA（加利福尼亚大学洛杉矶分校）
归纳不变量的自动综合是软件验证中的一个重要问题。一旦所有的不变量都被指定，软件验证就简化为验证条件的检查。虽然静态分析来推断不变量已经被研究了四十多年，但近年来出现了一系列数据驱动的不变量推断技术，这些技术从示例中猜测不变量，而不是分析程序文本。然而，这些技术已经被证明只能扩展到具有少量变量的程序。在本文中，我们研究了这些可扩展性问题，并在我们的工具绿洲中解决了这些问题，该工具绿洲提高了数据驱动的不变推理的规模，并在基准测试中优于最先进的系统。
2020-07-16 cs.LG cs.PL cs.SE
