5 papers
Soteria: Efficient Symbolic Execution as a Functional Library
Sacha-Ãlie Ayoun, Opale Sjöstedt, Azalea Raad
Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach…
Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees, Extended Version
Nat Karmios, Sacha-Ãlie Ayoun, Philippa Gardner
In recent years, compositional symbolic execution (CSE) tools have been growing in prominence and are becoming more and more applicable to real-world codebases. Still to this day,…
Compositional Symbolic Execution for the Next 700 Memory Models (Extended Version)
Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho +3
Multiple successful compositional symbolic execution (CSE) tools and platforms exploit separation logic (SL) for compositional verification and/or incorrectness separation logic (I…
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…
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Ãlie Ayoun +3
The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that c…