Using History Invariants to Verify Observers

DOI10.1007/978-3-540-71316-6_7zbMath1187.68156OpenAlexW2100878175MaRDI QIDQ5756488

K. Rustan M. Leino, Wolfram Schulte

Publication date: 4 September 2007

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71316-6_7

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Holistic Specifications for Robust Programs ⋮ Verification of mutable linear data structures and iterator-based algorithms in Dafny ⋮ Automatic verification of Java programs with dynamic frames

Uses Software

• Spec#
• SIMPLIFY
• Boogie

This page was built for publication: Using History Invariants to Verify Observers