Enforcing structural invariants using dynamic frames

DOI10.1007/978-3-642-19835-9_8MaRDI QIDQ3000638zbMATH OpenOpenAlexFDO

Authors Diego Garbervetsky, Daniel Gorín, Ariel Neisen

Publication date 19 May 2011

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19835-9_8

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• The dynamic frames theory
• Dynamic frames in Java dynamic logic
• Automatic verification of Java programs with dynamic frames
• Abstract dynamic frames
• Generalized arrays for Stainless frames

Cites work

• scientific article; zbMATH DE number 1304000 (Why is no real title available?)
• A Basis for Verifying Multi-threaded Programs
• Automated Deduction – CADE-20
• Dafny: an automatic program verifier for functional correctness
• The dynamic frames theory
• Verifying properties of well-founded linked lists

Cited in

(3)

• The dynamic frames theory
• Automatic verification of Java programs with dynamic frames
• Dynamic frames in Java dynamic logic

Describes a project that uses

Uses Software

• VeriCool
• Spec#
• Dafny

This page was built for publication: Enforcing structural invariants using dynamic frames

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