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

preconditionassertioninvariantseparation logicbehavioral subtypingpostconditionframe conditionsinterface specification languageSpec\#

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)

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

Describes a project that uses

Uses Software

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

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)