2 citations · 4 across the 4 of their papers we have counts for
5 papers
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…
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…
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…
Exact Separation Logic (Extended Version)
Petar Maksimović, Caroline Cronjäger, Andreas Lööw +2
Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised,…