24 citations · 28 across the 2 of their papers we have counts for
3 papers
cs.LO2023★ 24 cited
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…
cs.CR2022
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…
cs.LO2022★ 4 cited
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 (…