5 citations · 13 across the 8 of their papers we have counts for
5 papers · 1 filter
A Hoare Logic with Regular Behavioral Specifications
Gidon Ernst, Alexander Knapp, Toby Murray
We present a Hoare logic that extends program specifications with regular expressions that capture behaviors in terms of sequences of events that arise during the execution. The id…
Deductive Verification via the Debug Adapter Protocol
Gidon Ernst, Johannes Blau, Toby Murray
We propose a conceptual integration of deductive program verification into existing user interfaces for software debugging. This integration is well-represented in the "Debug Adapt…
An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More
Toby Murray
Recently, authors have proposed under-approximate logics for reasoning about programs. So far, all such logics have been confined to reasoning about individual program behaviours.…
VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices)
Daniel Schoepe, Toby Murray, Andrei Sabelfeld
Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the past four decades. Despite an impressive array of w…
VST-Flow: Fine-grained low-level reasoning about real-world C code
Samuel Gruetter, Toby Murray
We show how support for information-flow security proofs could be added on top of the Verified Software Toolchain (VST). We discuss several attempts to define information flow secu…