3 papers
cs.SE2026
Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia
Lea Salome Brugger, Xavier Denis, Peter Müller
Deductive verification is an effective method to ensure that a given system exposes the intended behavior. In spite of its proven usefulness and feasibility in selected projects, d…
cs.PL2025
A Hybrid Approach to Semi-automated Rust Verification
Sacha-Ãlie Ayoun, Xavier Denis, Petar MaksimoviÄ +1
We propose a hybrid approach to end-to-end Rust verification where the proof effort is split into powerful automated verification of safe Rust and targeted semi-automated verificat…
cs.PL2024
Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
Federico Poli, Xavier Denis, Peter Müller +1
Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not…