Behavioral interface specification languages

DOI10.1145/2187671.2187678MaRDI QIDQ2875082zbMATH OpenOpenAlexWikidataFDO

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

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

assertionbehavioral subtypingframe conditionsinterface specification languageinvariantpostconditionpreconditionseparation logicSpec\#

Mathematics Subject Classification ID

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

Recommendations

• Writing Larch interface language specifications
• Mining specifications
• scientific article; zbMATH DE number 1860624
• Protective interface specifications
• Behavioral program logic

Cited in

(14)

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

Describes a project that uses

Uses Software

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

This page was built for publication: Behavioral interface specification languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2875082)