24 citations · 28 across the 3 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
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.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 (…
cs.LO2022
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…