Verification of object-oriented programs: a transformational approach

DOI10.1016/J.JCSS.2011.08.002MaRDI QIDQ439944zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

aliasinginheritancesubtypingprogram verificationrecursive programsnull referencesobject-oriented programsrelative completenessstrong partial correctnesssyntax-directed transformation

Mathematics Subject Classification ID

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)

Recommendations

• Program derivation with verified transformations — a case study
• scientific article; zbMATH DE number 860045
• scientific article; zbMATH DE number 3872657
• Modular specification and verification of object-oriented programs
• Modular specification and verification of object-oriented programs

Cites work

• scientific article; zbMATH DE number 3688676 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3767008 (Why is no real title available?)
• scientific article; zbMATH DE number 192929 (Why is no real title available?)
• scientific article; zbMATH DE number 1105469 (Why is no real title available?)
• scientific article; zbMATH DE number 1759367 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• A Proof System for Communicating Sequential Processes
• A logic of object-oriented programs
• A proof outline logic for object-oriented programming
• A structural approach to operational semantics
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Hoare logic for Java in Isabelle/HOL
• Modular invariants for layered object structures
• Ownership confinement ensures representation independence for object-oriented programs
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Proving total correctness of recursive procedures
• Soundness and Completeness of an Axiom System for Program Verification
• Verification of sequential and concurrent programs
• Verifying properties of parallel programs
• Weakest pre-condition reasoning for Java programs with JML annotations

Cited in

(13)

• Specification and verification of object-oriented programs using supertype abstraction
• Tendencies in verifying object-oriented software
• Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
• Formal verification of object-oriented software. International conference, FoVeOOS 2010, Paris, France, June 28--30, 2010. Revised selected papers
• Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• A proof outline logic for object-oriented programming
• scientific article; zbMATH DE number 860045 (Why is no real title available?)
• An operational semantics for object-oriented concepts based on the class hierarchy
• Fifty years of Hoare's logic
• Modular specification and verification of object-oriented programs
• Proof pearl: The KeY to correct and stable sorting
• Weak arithmetic completeness of object-oriented first-order assertion networks
• scientific article; zbMATH DE number 1860624 (Why is no real title available?)

Describes a project that uses

Uses Software

• Modula
• Eiffel
• JML
• Boogie

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)