Verification of object-oriented programs: a transformational approach
DOI10.1016/J.JCSS.2011.08.002zbMATH Open1245.68062OpenAlexW1489237563MaRDI QIDQ439944FDOQ439944
Authors: Krzysztof R. Apt, Frank S. de Boer, Stijn De Gouw, Ernst-Rüdiger Olderog 
Publication date: 17 August 2012
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jcss.2011.08.002
Recommendations
aliasinginheritancesubtypingprogram verificationrecursive programsnull referencesobject-oriented programsrelative completenessstrong partial correctnesssyntax-directed transformation
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A structural approach to operational semantics
- An axiomatic basis for computer programming
- Verifying properties of parallel programs
- Soundness and Completeness of an Axiom System for Program Verification
- Title not available (Why is that?)
- An axiomatic proof technique for parallel programs
- Ownership confinement ensures representation independence for object-oriented programs
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Hoare logic for Java in Isabelle/HOL
- A logic of object-oriented programs
- Title not available (Why is that?)
- Verification of sequential and concurrent programs
- Weakest pre-condition reasoning for Java programs with JML annotations
- Modular invariants for layered object structures
- A proof outline logic for object-oriented programming
- Title not available (Why is that?)
- A Proof System for Communicating Sequential Processes
- Title not available (Why is that?)
- Proving total correctness of recursive procedures
Cited In (13)
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
- Weak arithmetic completeness of object-oriented first-order assertion networks
- Title not available (Why is that?)
- Proof pearl: The KeY to correct and stable sorting
- Tendencies in verifying object-oriented software
- Fifty years of Hoare's logic
- Title not available (Why is that?)
- An operational semantics for object-oriented concepts based on the class hierarchy
- Specification and verification of object-oriented programs using supertype abstraction
- Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
- Formal verification of object-oriented software. International conference, FoVeOOS 2010, Paris, France, June 28--30, 2010. Revised selected papers
- A proof outline logic for object-oriented programming
- Modular specification and verification of object-oriented programs
Uses Software
This page was built for publication: Verification of object-oriented programs: a transformational approach
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q439944)
