Dynamic Frames in Java Dynamic Logic

DOI10.1007/978-3-642-18070-5_10zbMath1308.68046OpenAlexW1624683186MaRDI QIDQ3067542

Benjamin Weiß, Mattias Ulbrich, Peter H. Schmitt

Publication date: 21 January 2011

Published in: Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-18070-5_10

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Abstraction and subsumption in modular verification of C programs, Stateful Behavioral Types for Active Objects

Cites Work

• Unnamed Item
• Modular invariants for layered object structures
• Proof of correctness of data representations
• Specification and verification challenges for sequential object-oriented programs
• Guarded commands, nondeterminacy and formal derivation of programs
• Separation logic and abstraction
• Algebraic Methodology and Software Technology
• Sequential, Parallel, and Quantified Updates of First-Order Structures