20 citations · 50 across the 12 of their papers we have counts for
12 papers
Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version)
Toby Murray, Mukesh Tiwari, Gidon Ernst +1
We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the prob…
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…
State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing
Dongge Liu, Van-Thuan Pham, Gidon Ernst +2
The statefulness property of network protocol implementations poses a unique challenge for testing and verification techniques, including Fuzzing. Stateful fuzzers tackle this chal…
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…
Compositional Vulnerability Detection with Insecurity Separation Logic (Extended Version)
Toby Murray, Pengbo Yan, Gidon Ernst
Memory-safety issues and information leakage are known to be depressingly common. We consider the compositional static detection of these kinds of vulnerabilities in first-order C-…
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…