ABSTRACT. The demonstrated code‑understanding capabilities of large language models (LLMs) raise the question of whether they can be used for automated program verification—a task that typically demands high‑level, abstract reasoning about program properties, which remains challenging for existing verification tools. In this talk, we overview several research directions, developed over the past two years, that propose methodologies for combining the strengths of LLMs and automated reasoners in program verification. We then take a closer look at Lemur, a tool that formally describes such a methodology as a set of derivation rules and proves its soundness. Lemur instantiates the calculus as a sound automated verification procedure and demonstrates practical improvements on a suite of synthetic and competition benchmarks.

ABSTRACT. In many applications, SMT solvers are utilized to solve similar or identical tasks over time. Significant variations in performance due to small changes in the input are not uncommon and lead to frustration for users. This sort of stability problem represents an important usability challenge for SMT solvers. We introduce an approach for mitigating the stability problem based on normalizing solver inputs. We show that a perfect normalizing algorithm exists but is computationally expensive. We then describe an approximate algorithm and evaluate it on a set of benchmarks from related work, as well as a large set of benchmarks sampled from SMT-LIB. Our evaluation shows that our approximate normalizer reduces runtime variability with minimal overhead and is able to normalize a large class of mutated benchmarks to a unique normal form.

ABSTRACT. In this paper, we investigate customizing the solving strategy for an individual SMT problem, based solely on the problem itself, without relying on any offline strategy tuning. Our key insight is to generate a set of subproblems derived from the original formula, analyze the behavior of candidate solving strategies on these smaller, representative subproblems, and predict which strategy will perform best on the original formula. We demonstrate that performance on the subproblems is frequently indicative of performance on the original formula. Additionally, we introduce a novel subproblem generation procedure that outperforms existing SMT formula partitioning techniques for the proposed workflow. Finally, we show that on a selection of SMT-LIB benchmarks, when our approach can make a prediction, it can reduce the total compute time substantially.

ABSTRACT. Many real applications problems can be encoded easily as quantified formulas in SMT. However, this simplicity comes at the cost of difficulty during solving by SMT solvers. Different strategies and quantifier instantiation techniques have been developed to tackle this. However, SMT solvers still struggle with quantified formulas generated by some applications. In this paper, we discuss the use of set-bounded quantifiers, quantifiers whose variable ranges over a finite set. These quantifiers can be implemented using quantifier-free fragment of the theory of finite relations with a filter operator. We show that this approach outperforms other quantification techniques in satisfiable problems generated by the SLEEC tool, and is very competitive on unsatisfiable benchmarks compared to LEGOS, a specialized solver for SLEEC. We also identify a decidability class of constraints with restricted applications of the filter operator, while showing that unrestricted applications lead to undecidability.

ABSTRACT. State-of-the-art Boolean satisfiability (SAT) solvers increasingly use techniques beyond resolution. One of the strongest such techniques is Propagation Redundancy (PR) learning. Solvers utilizing PR learning may admit short proofs for benchmark families with exponentially large resolution proofs, including pigeonhole and mutilated chessboard. However, existing PR clause learning techniques require an NP-hard check; hence, they are computationally expensive and difficult to add to existing tools.

We propose a new technique for learning PR clauses based on conditional autarkies and implement it in the SAT solver \cadical. Our method is modular, allowing for cross-solver compatibility, and learns PR clauses in linear time. Additionally, we introduce a number of heuristics, including a clause-shrinking technique and filtering to avoid trivial PR clauses, ensuring that our method learns useful clauses. We show that this is competitive with state-of-the-art PR clause learning techniques, and improves performance on a portion of SAT competition benchmarks.

ABSTRACT. Program synthesis is the task of automatically constructing a program conforming to a given specification. In this paper we focus on synthesis of single-invocation recursion-free functions conforming to a specification given as a logical formula in the presence of uncomputable symbols (i.e., symbols used in the specification but not allowed in the resulting function). We approach the problem via SMT-solving methods: we present a quantifier elimination algorithm using model-based projections for both total and partial function synthesis, working with theories of uninterpreted functions and linear arithmetic and their combination. For this purpose we also extend model-based projection to produce witnesses for these theories. Further, we present procedures tailored for the case of uniquely determined solutions. We implemented a prototype of the algorithms using the SMT-solver Z3, demonstrating their practical efficiency compared to the state of the art.

ABSTRACT. Pre-trained large language models (LLMs) have recently attracted huge attention in program synthesis with natural language specifications. However, in invariant synthesis, the most effective tools still rely on brute-force methods such as Daikon, Houdini, enumerative algorithms, DistAI, or traditional machine learning approaches like ICE. In this paper, we investigate the capabilities of LLMs in invariant synthesis by creating a specialized set of prompts. When one-shot invariant synthesis fails, we introduce two revision frameworks of incorporating LLM calls. In the first framework, the synthesizer provides the LLM with its current invariant and the information of counterexamples, and the LLM offers guidance on atomic predicates for reconstructing the invariants. The second framework uses the LLM to generate invariants by itself within a revision process. We tested our methods on 16 distributed systems modeled in Promela and verified them with Spin. Our results show that GPT-4.0, whether used alone or in a revision framework, is less effective than state-of-the-art invariant synthesis methods. However, our integrated approach, which employs the LLM as a predicate prompter, significantly outperforms both the self-revised LLM framework and the symbolic invariant synthesizer. This integrated technique also produces higher-quality invariants in general. Because we focus on system traces, we primarily consider likely invariants. However, our revision frameworks can also learn true invariants by using model checkers in the revision frameworks.

ABSTRACT. Hardware verification is essential to ensure that hardware designs meet their design specifications and function as intended. However, use of formal verification requires extensive manual work in order to write formal specifications. Specification mining aims to alleviate this manual burden, with conventional techniques using statistical methods and pattern matching to generate likely specifications from sample execution traces from the hardware. A limitation of this is that the quality of the specifications is determined by the quality of the traces. In this paper, we present an approach to using oracle-guided synthesis to generate specifications for hardware, using counterexamples and negative examples to refine specifications generated based on traces. We evaluate our approach on real-world Verilog benchmarks and demonstrate that specifications generated by our tool can detect high proportions of hardware mutations.

ABSTRACT. Many software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Program verifiers for mainstream languages, however, are customized for individual languages. Verification by compiling to a common encoding requires supporting full language syntax/semantics -- this is prohibitive for modern languages. We present PolyVer, an alternative approach to polyglot verification that bootstraps off-the-shelf language-specific verifiers with abstraction, compositional reasoning, and synthesis. PolyVer uses contracts written in an intermediate language to abstract individual procedures in the system. Verification integrates (a) language-specific verifiers (e.g. for C or Rust) to validate these contracts with (b) a model checker for verifying the overall system using the contracts. The intermediate language sidesteps the need for compiling implementation languages to a common encoding, a key obstacle with polyglot verification. Finally, PolyVer addresses the challenge of manually writing contracts by automatically synthesizing contracts using a large-language-model (LLM) based synthesizer. Overall PolyVer performs contract synthesis and verification in CEGIS-CEGAR loop to verify the system-level property. We use PolyVer to verify programs in the Lingua Franca polyglot language. We are able to verify systems with C and Rust procedures, as well as C language fragments that were unsupported in previous work.

ABSTRACT. The correct management of translation lookaside buffers (TLBs) by memory-management software is critical to the security of modern computer systems. We develop a methodology for reasoning about software that modifies address translations executing on machines with a TLB, enabling the verification of binary-level, security-critical, memory-management code in operating system kernels. We automate proving that the TLB does not contain entries that are inconsistent with the page tables which allows us to reduce the problem of reasoning about address translation in the presence of a TLB to the problem of reasoning about address translation by walking page tables. Our technique is independent of any particular ISA or TLB microarchitecture. To demonstrate the effectiveness of our approach, we add a TLB to the ACL2 model of the x86 ISA, implement this reasoning technique in the ACL2 theorem prover, and verify a page-table-altering program called Zero-Copy that copies a page of data in a virtual-address space by modifying the page tables. We were able to reuse and update a previous version of the proof of correctness that was performed with a version of the x86 ISA model lacking a TLB, confirming the effectiveness of our reduction-based method.