Verification of object-oriented programs: a transformational approach

DOI10.1016/j.jcss.2011.08.002zbMath1245.68062OpenAlexW1489237563MaRDI QIDQ439944

Krzysztof R. Apt, Stijn De Gouw, Frank S. de Boer, Ernst-Ruediger 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

zbMATH Keywords

inheritancerelative completenessaliasingsubtypingprogram verificationrecursive programsnull referencesobject-oriented programsstrong partial correctnesssyntax-directed transformation

Mathematics Subject Classification ID

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

Related Items (3)

Fifty years of Hoare's logic ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Proof pearl: The KeY to correct and stable sorting

Uses Software

• Modula
• Eiffel
• JML
• Boogie

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verification of sequential and concurrent programs
• Proving total correctness of recursive procedures
• An axiomatic proof technique for parallel programs
• A structural approach to operational semantics
• Weakest pre-condition reasoning for Java programs with JML annotations
• Modular invariants for layered object structures
• A proof outline logic for object-oriented programming
• Ownership confinement ensures representation independence for object-oriented programs
• A Proof System for Communicating Sequential Processes
• Verifying properties of parallel programs
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Hoare logic for Java in Isabelle/HOL
• Verification: Theory and Practice
• An axiomatic basis for computer programming

This page was built for publication: Verification of object-oriented programs: a transformational approach