20 citations · 25 across the 8 of their papers we have counts for
9 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,…
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +3
Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust,…
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…
Reinforcement Learning with Formal Performance Metrics for Quadcopter Attitude Control under Non-nominal Contexts
Nicola Bernini, Mikhail Bessa, Rémi Delmas +5
We explore the reinforcement learning approach to designing controllers by extensively discussing the case of a quadcopter attitude controller. We provide all details allowing to r…