Towards Trace-based Deductive Verification (Tech Report)

Richard Bubel, Dilian Gurov, Reiner Hähnle +1

Contracts specifying a procedure's behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events o…