Automatic verification of Java programs with dynamic frames
DOI10.1007/S00165-010-0148-1zbMATH Open1204.68131OpenAlexW2069522167MaRDI QIDQ973055FDOQ973055
Authors: Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte 
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
Recommendations
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cites Work
- Programming Languages and Systems
- Modular specification and verification of object-oriented programs
- Specification and verification challenges for sequential object-oriented programs
- Lazy behavioral subtyping
- Mathematics of Program Construction
- Automatic verification of Java programs with dynamic frames
- Separation logic, abstraction and inheritance
- Protective interface specifications
- Using History Invariants to Verify Observers
Cited In (12)
- Programming Languages and Systems
- The dynamic frames theory
- Automatic verification of Java programs with dynamic frames
- Dynamic frames in Java dynamic logic
- Enforcing structural invariants using dynamic frames
- Generalized arrays for Stainless frames
- Certified abstract cost analysis
- Theorem Proving in Higher Order Logics
- Verification of Concurrent Systems with VerCors
- Unifying separation logic and region logic to allow interoperability
- Holistic Specifications for Robust Programs
- Model Checking Software
Uses Software
This page was built for publication: Automatic verification of Java programs with dynamic frames
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q973055)
