Deductive verification is an approach where the user expends effort in constructing a program invariant manually, or learns this invariant from program traces, and subsequently uses the program invariant for safety verification tasks. Most existing invariant synthesis tools still rely on model checking methods to certify invariants, use enumerative search to identify and refine candidate invariants, and user insights to start with a set of candidate predicates that may appear in the final (learned) invariant. On the other hand, pre-trained large language models (LLMs) have recently attracted considerable attention in various tasks related to generating program code (e.g., from natural language). There have been recent efforts at applying LLMs to the program verification context. In this paper, we investigate the capabilities of LLMs to synthesize program invariants by creating a specialized set of prompts. When LLM invariant synthesis with direct prompting fails, we introduce two revision frameworks for incorporating LLM calls. In the first framework PSyn, the LLM suggests atomic predicates based on counterexamples for reconstructing the invariants. The second framework ISyn adopts the LLM to generate invariants by itself within a revision process. We tested our methods on 8 distributed systems modeled in Promela and invariants are verified with Spin. Our results show that the state-of-the-art model GPT-o3, when it is used to generate invariants directly, is less effective than the symbolic invariant synthesis method RunVS. However, our integrated approach PSyn, which employs the LLM as a predicate prompter, significantly outperforms GPT-o3 and ISyn and has comparable performance with RunVS. This integrated technique also produces higher-quality invariants in general. Because we focus on runtime monitoring frameworks, we primarily consider system traces and hence likely invariants. However, our revision frameworks can also learn true invariants by using model checkers in the revision frameworks.
We present a formal executable model of CHERI architectural features integrated with a formalized Y86 ISA. CHERI is an extension of conventional hardware ISAs centralized around capabilities, which are descriptions of permissions at the hardware level that can be used in place of pointers. CHERI enables fine-grained memory protection and highly scalable soft-ware compartmentalization to mitigate security vulnerabilities beyond what can be done by current architectures. We use our formal model to prove the memory protection and security features of CHERI itself, prototype extensions to CHERI, and verify the correctness of machine code involving capabilities. Since it is executable, our model also serves as a symbolic simulator of a CHERI augmented x86-like processor, allowing step-by-step validation of CHERI capability features in a controlled, formal environment. We are motivated by the adoption of CHERI by industry leaders that design real-world hardware, the need for industrial-strength tools to perform formal CHERI analyses, and the current development of CHERI extensions to x86 platforms. We build our model in an all-in-one first-order logic and program-ming system. Our model enables formal verification of CHERI designs and the rapid-prototyping of new CHERI architectural features, and we apply existing industry push-button verification tools and custom heuristics to prove the correctness of CHERI artifacts.
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 that uses 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.
This paper presents a framework for quantifying robustness of U-Nets, a widely used neural network architecture in 3 dimensional biomedical image segmentation. We first present a metric for measuring robustness of biomedical image segmentation methods. We then propose TensorStars, a new representation to model the perturbation of a given medical image and overapproximate the effect of these perturbations on the image segmentation performed by a 3 dimensional UNet. Given the large dimensionality of medical images, naive implementation of overapproximation results in poor scalability of robustness verification. We propose two main improvements, (1) leveraging hardware acceleration from GPUs for performing tensor operations, and (2) leverage the CPU parallelism for accelerating the ReLU overapproximation. We observe that these two enhancements improve the runtime by 10 x when implemented on a 32 core CPU with NVidia GeForce RTX with 8 GB VRam. We perform robustness analysis on a U-Net that performs segmentation of kidneys with cross entropy loss of less than 0.01. Our evaluation demonstrates that perturbing less than 3% of input voxels can result in misclassification of up to 20 % of voxels in the segmentation output. To the best of authors knowledge, this is the first work that extends the robustness verification of neural networks to biomedical imaging data.
There has been a massive amount of work on algorithms to verify and synthesize systems from temporal specifications. In contrast, there has been less work devoted to the problem of helping engineers to understand how and why their systems exhibit certain behaviors. Such understanding is important for them to debug, validate, and modify their implementations in response to changing needs. In this paper, we present one possible formalization of this problem as the task of recovering specifications that locally describe the behavior of individual parts of the circuit, given LTL specifications that globally describe the behavior of the entire circuit. We study the theoretical properties of these temporal subspecifications, and show that they are not always expressible in LTL, but can always be described by $\omega$-regular languages. We show that our algorithm can efficiently generate compact subspecifications when applied to benchmarks from the SYNTCOMP 2023 competition. Finally, through a user study, we show that subspecifications improve the accuracy of engineers by a factor of 17 when answering questions about these circuits.
The Realizable, Responsive, Unobtrusive Unit (R2U2) is a real-time, temporal logic-based runtime monitoring engine that has been successfully deployed on-board a wide range of cyber- physical systems, from aircraft to spacecraft to robots, checking in real time whether these systems uphold specified system requirements. However, the efficacy of deploying runtime monitors is highly sensitive to their correct configuration. Moreover, there are many barriers to adopting runtime monitors, including a high learning curve and the challenge of eliciting for-mal specifications that accurately capture system requirements. Therefore, we present the R2U2 Playground, an interactive web-based playground that provides visualization of R2U2. The R2U2 Playground provides stepwise execution coupled with reactive timeline plotting and visualization of its internal abstract syntax tree architecture. To this extent, the R2U2 Playground provides insight into how R2U2 evaluates specifications, allowing for easier specification understanding and debugging.
The Hardware Model Checking Competition 2025 (HWMCC'25) was the 13th competitive event for hardware model checkers. Affiliated to the 25th conference on Formal Methods in Computer-Aided Design 2025 (FMCAD'25) it took place in Menlo Park, California, USA, from Oct. 6 to 10, 2025.
This talk will cover the exciting progress made in the field of Program Synthesis over the years. Program synthesis is broadly concerned with generating programs from specifications. Program synthesis is a fascinating field since it encompasses a whole spectrum of problems that are obtained by just considering different notions of specifications and different classes of programs. We will discuss general approaches that have been developed, including bottom-up synthesis, top-down synthesis, and constraint-based synthesis. We will also cover some applications of program synthesis. The advent of large language models had an influence on the f ield, and in the second part of the talk, we will cover more recent work on program synthesis in this new age of large language models, along with the new opportunities it presents.
State-of-the-art Boolean satisfiability (SAT) solvers increasingly use techniques beyond resolution. One of the strongest such techniques is Propagation Redundant (PR) clause learning. Solvers utilizing PR clause 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.
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 the security-critical, memory-management code in operating system kernels at the binary level. 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 the virtual-address space by modifying the page tables. We were able to reuse and update substantial portions of 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.
In this tutorial, I will present techniques for automated formal verification of a variety of systems using Satisfiability Modulo Theories (SMT) solvers as main reasoning engines. The talk will focus mainly on the problem of verifying invariant properties on symbolic transition systems, but it will also cover techniques for the verification of Linear Time temporal logic (LTL) properties and extensions to deal with parameterized systems with an unbounded number of components. I will also introduce some concrete tools to solve Verification Modulo Theories problems automatically, and present a demo of their use in a realistic application.
The results of software verification are only as trustworthy as the provided specification. Errors or incompleteness in the specification can result in unwarranted confidence in the implementation. Previous work, particularly in the realm of model checking, has investigated a notion of coverage in verification. Portions of the system that could be replaced arbitrarily without causing verification failure are considered uncovered. We show that the same notion of coverage used in model checking can be applied to deductive software verification, with a reasonable performance penalty when using an implementation based on unsatisfiable cores. This approach provides opportunities for identifying specification gaps by detecting vacuous proofs, unconstrained code, and unnecessary or redundant specifications. We describe an implementation of this approach for the Boogie intermediate verification language, the use of this implementation from the verification-aware programming language Dafny, and experimental results on a large corpus of industry-scale Dafny code.
The Rust type system provides strong compile-time guarantees. However, some properties cannot be fully verified by the compiler. Specifically, properties like panic freedom and memory safety in mixed safe-unsafe code require verification beyond what the language enforces. We explore how to verify these properties in real-world Rust code using SeaBMC, a bounded model checker that ingests LLVM-IR generated by the Rust compiler. We demonstrate our approach through two case studies. In the first, we develop unit proofs for functional properties of four data-structure libraries: smallvec, tinyvec, seavec, and result-type from the Rust standard library. These unit proofs are checkable by both SeaBMC and Kani, a state-of-the-art bounded model checker for Rust, and we find that SeaBMC verifies these units an order of magnitude faster than Kani. The second case study focuses on verifying panic freedom of Wasmtime's Winch compiler. This application is driven by the requirement for high reliability when compiling WASM smart-contracts in the Stellar network. This case study highlights that executable counterexamples from SeaBMC are highly effective for localizing issues and discovering invariants. Our main contributions are (1) a new tool for Rust verification which, on our benchmarks, is an order of magnitude faster than Kani, (2) two case studies with reusable benchmarking and testing infrastructure, and (3) practical guidelines stemming from our experience verifying real-world code-bases.
The Student Forum at the International Conference on Formal Methods in Computer-Aided Design (FMCAD) gives undergraduate and graduate students the opportunity to introduce their research to the formal methods community and receive feedback. In 2025, the event took place in Menlo Park, California, USA. Twenty students were invited to give a short talk and present a poster of their work.
DQMax#SAT is a newly developed extension of Max#SAT that incorporates Henkin-type quantifiers and is utilized in function synthesis to enhance program security. This study refutes the earlier hypothesis that efficient reduction from DQMax#SAT to the dependency stochastic Boolean satisfiability (DSSAT) is not possible. We introduce a conversion algorithm that eliminates variables from dependency sets to achieve the reduction. Experimental results show that transforming DQMax#SAT formulas that encode function synthesis applications into DSSAT formulas and solving them using an off-the-shelf DSSAT solver yields superior results compared to directly solving them with the leading DQMax#SAT solver. This research not only clarifies the relationship between DQMax#SAT and DSSAT but also equips developers with conversion tools to assist in the evaluation of both DQMax#SAT and DSSAT solvers.
Cloud computing providers employ sophisticated authorization engines to decide when a request to access a resource should be allowed or denied. Several approaches have formalized the behavior of individual authorization policies, but authorization engines employ multiple types of policies that can interact in different ways. This paper presents a modular formalization of the Amazon Web Services (AWS) authorization engine and a corresponding analysis tool, called IAM-MULTIPOLICYANALYZER, for verifying properties pertaining to multiple policies of different types. IAM-MULTIPOLICYANALYZER adopts Zelkova[18]-i.e., the formalization of individual lAM policies as a basic building block, and uses a new domain-specific language for modularly describing how the authorization engine composes individual uses of Zelkova. As a result, IAM-MULTIPOLICYANALYZER provides a trusted, reusable, human-readable, and performant SMT-backed model of AWS's authorization logic that is now used within multiple AWS applications. We have run conformance testing of our model against the engine implementation and its documentation; the corner cases identified by our testing have led to improvements and modifications to the official AWS documentation.
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.
String constraint solving describes the problem of determining the satisfiability of first-order formulas where variables range over strings. Automated procedures for solving these problems are known as string solvers. Most existing solvers adopt a lazy SMT approach, where a SAT solver handles the Boolean structure of the formula and alternates with a specialized string reasoning engine, following the CDCL(T) paradigm. An alternative strategy, called eager SMT solving, reduces the entire problem to Boolean satisfiability, allowing it to be handled directly by a SAT solver. While successful eager approaches have been proposed, current implementations either lack expressiveness or are not publicly available. Here, we present a new eager string solver based on existing techniques, capable of solving Boolean combinations of word equations, regular constraints, and linear arithmetic over string lengths. An evaluation on the SMTLIB string benchmarks shows that our approach is competitive on a broad set of problems compared to state-of-the-art solvers, and even outperforms them in many cases. In particular, our solver demonstrates close to best-in-class performance on the SMT-COMP pure string benchmarks.
We introduce a novel encoding for Mission-time Linear Temporal Logic (MLTL), inspired by the recently-proposed Temporal Exponential Propagation method for learning finitetrace Linear Temporal Logic (LTLf) formulas. Our encoding translates MLTL formulas into bit-vector expressions whose size is $\mathcal{O}\left(n \log ^{2}(K)\right)$ with $n$ and $K$ being proportional to the formula size and largest temporal interval present in the formula respectively. We demonstrate how this encoding can be leveraged for two core applications: satisfiability checking and runtime monitoring. For satisfiability, our approach complements existing techniques by efficiently solving instances that are challenging for traditional encodings. For runtime monitoring, we show that our method achieves significantly higher throughput than current state-of-the-art tools, enabling faster and more scalable runtime verification in time-sensitive systems. Experimental results confirm that the proposed encoding and monitoring algorithm provide a practical and effective foundation for reasoning about MLTL properties, achieving 10.52 times higher throughput compared to state-of-the-art online techniques over a sample of pattern-instantiated formulas.
Rabbit is a modeling language for networked systems that allows processes and their communications to be programmed using familiar imperative constructs, while enabling various security assertions to be automatically verified via the Tamarin prover as a back-end. We propose an extension of Rabbit with general unbounded and nondeterministic loops, which are essential for modeling more realistic scenarios, along with optimization techniques that keep automatic verification via Tamarin tractable. We further introduce parameterized processes and communication channels, making Rabbit expressive enough to model systems such as a centralized server communicating with an unbounded number of client processes via a family of parameterized channels. We provide a proof-of-concept implementation of the extended Rabbit and present evaluation results.
