Invited Talk, Programming Languages and Verification Seminar @ Portland State University, USA, online (hybrid seminar)
In this invited talk, we present the first notion of completeness thresholds for memory safety proofs. They allow us to reduce unbounded memory safety proofs to bounded ones.
Poster, SPLASH 2023, Cascais, Portugal
With this poster, we present the first notion of completeness thresholds for program verification. They allow us to reduce unbounded memory safety proofs to bounded ones.
Invited Talk, Programming Group @ HSG, St. Gallen, Switzerland, St. Gallen, Switzerland
In this invited talk, we present the first notion of completeness thresholds for memory safety proofs. They allow us to reduce unbounded memory safety proofs to bounded ones.
Talk, CAV 2021, online (virtual conference)
We propose the first separation logic to modularly verify termination of busy-waiting. We achieve this by introducing a novel type of ghost resource, called ghost signals.
Talk, FTfJP 2020, online (virtual workshop)
In this talk we present our work on verifying termination of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen. Further, we outline our plans to generalize this approach to verify termination of busy-waiting for arbitrary events.
Talk, Student Research Competition @ POPL 2019, Cascais, Portugal
We propose a language design which makes latency and locations explicit and extracts static type-level bounds for a computation’s runtime latency.