24 citations · 28 across the 3 of their papers we have counts for
4 papers
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
Thibault Dardinier, Peter Müller
Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (suc…
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
Marco Eilers, Thibault Dardinier, Peter Müller
Information flow security ensures that the secret data manipulated by a program does not influence its observable output. Proving information flow security is especially challengin…
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (…
Sound Automation of Magic Wands (extended version)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks +2
The magic wand (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance…