Combining Axiomatic Models for Refinement Proofs

Suha Orhun Mutluergil, Alperen Dogan

Refinement proofs verify an implementation by showing that its behaviours are subsumed by a simpler specification, on which safety properties are easier to establish. We study how…