Counterexample-Guided k-Induction Verification for Fast Bug Detection

Bonsai: Synthesis-Based Reasoning for Type Systems

We describe algorithms for symbolic reasoning about executable models of type systems, supporting three queries intended for designers of type systems. First, we check for type soundness bugs and synthesize a counterexample program if such a bug is found. Second, we compare two versions of a type system, synthesizing a program accepted by one but rejected by the other. Third, we minimize the size of synthesized counterexample programs. These algorithms symbolically evaluate typecheckers and interpreters, producing formulas that characterize the set of programs that fail or succeed in the typec…

Combining k-Induction with Continuously-Refined Invariants

Bounded model checking (BMC) is a well-known and successful technique for finding bugs in software. k-induction is an approach to extend BMC-based approaches from falsification to verification. Automatically generated auxiliary invariants can be used to strengthen the induction hypothesis. We improve this approach and further increase effectiveness and efficiency in the following way: we start with light-weight invariants and refine these invariants continuously during the analysis. We present and evaluate an implementation of our approach in the open-source verification-framework CPAchecker. …

面向并发的无回归综合

Regression-free Synthesis for Concurrency

在修复并发错误的同时，程序修复算法可能会引入新的并发错误。我们提出了一个算法，避免这种回归。解决方案的空间是由一组程序转换，我们认为在修复过程。这些包括在线程内重新排序指令和插入原子部分。新算法从正例（无错误迹）和反例（错误迹）中学习候选解空间上的约束。从每个反例中，算法学习一个必要的约束来消除错误。从每个肯定的例子中，它学习一个必要的约束，以防止修复将跟踪变成错误跟踪。我们实现了该算法，并评估了简化的Linux设备驱动程序与已知的错误。

Complexity and Information in Invariant Inference

This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We analyze the complexity of this problem in a black-box model, called the Hoare-query model, which is general enough to capture algorithms such as IC3/PDR and its variants. An algorithm in this model learns about the system's reachable states by querying the validity of Hoare triples. We show that in general an algorithm in the Hoare-query model requir…

神经形式化验证：智能体的语言无关形式化程序推理

Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning

该研究提出神经形式化验证（NFV），让AI编码智能体与成熟验证器结合，为主流语言开发者实现一键式程序验证，在Python编程问题数据集上取得了良好的验证效果。

CIR+CVN：连接LLM语义理解与Petri网验证以实现并发程序

CIR+CVN: Bridging LLM Semantic Understanding and Petri-Net Verification for Concurrent Programs

本文提出CIR+CVN框架，通过LLM生成并发抽象模型，结合Petri网验证并发程序，实现迭代调试与修复，提升并发程序的可靠性。