20 citations · 50 across the 12 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…
Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions
Gidon Ernst
Cuvée is a program verification tool that reads SMT-LIB-like input files where terms may additionally contain weakest precondition operators over abstract programs. Cuvée translate…
A Complete Approach to Loop Verification with Invariants and Summaries
Gidon Ernst
Invariants are the predominant approach to verify the correctness of loops. As an alternative, loop contracts, which make explicit the premise and conclusion of the underlying indu…
A Formal Model of a Virtual Filesystem Switch
Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg +2
This work presents a formal model that is part of our effort to construct a verified file system for Flash memory. To modularize the verification we factor out generic aspects into…