The dynamic frames theory

DOI10.1007/S00165-010-0152-5MaRDI QIDQ539422zbMATH OpenOpenAlexFDO

Authors I. T. Kassios

Publication date 30 May 2011

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-010-0152-5

zbMATH Keywords

frame problemspecification languages

Mathematics Subject Classification ID

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

Recommendations

• Enforcing structural invariants using dynamic frames
• Dynamic frames in Java dynamic logic
• Abstract dynamic frames
• An Outline of a Dynamic Theory of Frames
• Automatic verification of Java programs with dynamic frames

Cites work

• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• scientific article; zbMATH DE number 3359806 (Why is no real title available?)
• A Basis for Verifying Multi-threaded Programs
• A Theory of Pointers for the UTP
• Automatic verification of Java programs with dynamic frames
• Mathematics of Program Construction
• Modular specification of frame properties in JML
• Programming Languages and Systems
• Separation and information hiding
• Separation logic and abstraction
• Unifying theories of locations

Cited in

(14)

• Schematic program proofs with abstract execution. Theory and applications
• Verifying Whiley programs with Boogie
• Capturing dynamic conceptual frames
• Laws of programming for references
• Automatic verification of Java programs with dynamic frames
• Dynamic boundaries: information hiding by second order framing with first order assertions
• Dynamic frames in Java dynamic logic
• An Outline of a Dynamic Theory of Frames
• Reasoning about separation using abstraction and reification
• Enforcing structural invariants using dynamic frames
• Abstract dynamic frames
• We-thinking and vacillation between frames: filling a gap in Bacharach's theory
• Unifying separation logic and region logic to allow interoperability
• A first-order logic with frames

Describes a project that uses

Uses Software

• VeriCool
• Boogie

This page was built for publication: The dynamic frames theory

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