3 citations · 3 across the 4 of their papers we have counts for
4 papers
The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics
Eduard Kamburjan, Nathan Wasser
We present a novel and well automatable approach to formal verification of C programs with underspecified semantics, i.e., a language semantics that leaves open the order of certai…
Deductive Verification of Programs with Underspecified Semantics by Model Extraction
Eduard Kamburjan, Nathan Wasser
We present a novel and well automatable approach to formal verification of programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain…
Treating for-Loops as First-Class Citizens in Proofs
Nathan Wasser, Dominic Steinhöfel
Indexed loop scopes have been shown to be a helpful tool in creating sound loop invariant rules in dynamic logic for programming languages with abrupt completion, such as Java. The…
Technical Report: Using Loop Scopes with for-Loops
Nathan Wasser, Dominic Steinhöfel
Loop scopes have been shown to be a helpful tool in creating sound loop invariant rules which do not require program transformation of the loop body. Here we extend this idea from…