Behavioral interface specification languages

DOI10.1145/2187671.2187678zbMath1293.68078OpenAlexW2095907349MaRDI QIDQ2875082

Matthew J. Parkinson, John Hatcliff, Peter Müller, K. Rustan M. Leino, Gary T. Leavens

Publication date: 13 August 2014

Published in: ACM Computing Surveys (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2187671.2187678

zbMATH Keywords

preconditioninvariantassertionseparation logicbehavioral subtypingpostconditionframe conditionsinterface specification languageSpec\#

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

Skill-Based Verification of Cyber-Physical Systems ⋮ Holistic Specifications for Robust Programs ⋮ Formal specification and verification of JDK's identity hash map implementation ⋮ Modular inference of subprogram contracts for safety checking ⋮ Interface automata for shared memory ⋮ Verification of mutable linear data structures and iterator-based algorithms in Dafny ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ The spirit of ghost code ⋮ Loop invariants ⋮ Verifying traits: an incremental proof system for fine-grained reuse ⋮ An abstract contract theory for programs with procedures ⋮ Richer interface automata with optimistic and pessimistic compatibility

Uses Software

• CUTE
• Isabelle/HOL
• LARCH
• CASL
• SLAM
• KRAKATOA
• SPIN
• ACSL
• Spec#
• Uppaal
• cvc3
• z3
• VCC
• VeriFast
• Boogie
• LUSTRE
• VeriCool
• HighSpec

This page was built for publication: Behavioral interface specification languages