3 citations · 7 across the 10 of their papers we have counts for
11 papers
Kani: A Model Checker for Rust
Rémi Delmas, Zyad Hassan, Qinheping Hu +9
Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw p…
Verifying the Rust Standard Library
Byron Cook, Remi Delmas, Zyad Hassan +9
Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic…
Teaching LLMs Program Semantics via Symbolic Execution Traces
Jonas Bayer, Stefan Zetzsche, Olivier Bouissou +3
We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025,…
A Neurosymbolic Approach to Natural Language Formalization and Verification
Chenyang An, Sam Bayless, Stefano Buliani +27
Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries l…
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
Romy Peled, Daniel Kroening, Michael Tautschnig +1
Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and th…
Neural Model Checking
Mirco Giacobbe, Daniel Kroening, Abhinandan Pal +1
We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every ex…
CBMC: The C Bounded Model Checker
Daniel Kroening, Peter Schrammel, Michael Tautschnig
The C Bounded Model Checker (CBMC) demonstrates the violation of assertions in C programs, or proves safety of the assertions under a given bound. CBMC implements a bit-precise tra…
Assisted Coverage Closure
Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy +3
The malfunction of safety-critical systems may cause damage to people and the environment. Software within those systems is rigorously designed and verified according to domain spe…
On the Structure and Complexity of Rational Sets of Regular Languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig +1
In a recent thread of papers, we have introduced FQL, a precise specification language for test coverage, and developed the test case generation engine FShell for ANSI C. In essenc…
Partial Orders for Efficient BMC of Concurrent Software
Jade Alglave, Daniel Kroening, Michael Tautschnig
The vast number of interleavings that a concurrent program can have is typically identified as the root cause of the difficulty of automatic analysis of concurrent software. Weak m…
Software Verification for Weak Memory via Program Transformation
Jade Alglave, Daniel Kroening, Vincent Nimal +1
Despite multiprocessors implementing weak memory models, verification methods often assume Sequential Consistency (SC), thus may miss bugs due to weak memory. We propose a sound tr…