Automatic verification of Java programs with dynamic frames

DOI10.1007/s00165-010-0148-1zbMath1204.68131OpenAlexW2069522167MaRDI QIDQ973055

Bart Jacobs, Wolfram Schulte, Frank Piessens, Jan Smans

Publication date: 28 May 2010

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

Full work available at URL: https://doi.org/10.1007/s00165-010-0148-1

zbMATH Keywords

frame problemdata abstractionprogram verificationdynamic frames

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (7)

Holistic Specifications for Robust Programs ⋮ Generalized arrays for Stainless frames ⋮ The dynamic frames theory ⋮ Verification of Concurrent Systems with VerCors ⋮ Automatic verification of Java programs with dynamic frames ⋮ Unifying separation logic and region logic to allow interoperability ⋮ Certified abstract cost analysis

Uses Software

• Spec#
• z3
• VeriFast
• Boogie
• jStar
• Featherweight Java
• MJ

Cites Work

• Lazy behavioral subtyping
• Automatic verification of Java programs with dynamic frames
• Protective interface specifications
• Specification and verification challenges for sequential object-oriented programs
• Separation logic, abstraction and inheritance
• Mathematics of Program Construction
• Programming Languages and Systems
• Using History Invariants to Verify Observers
• Modular specification and verification of object-oriented programs

This page was built for publication: Automatic verification of Java programs with dynamic frames