Modular specification and verification of object-oriented programs

zbMath0998.68034MaRDI QIDQ5960651

Peter Müller

Publication date: 15 April 2002

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

specificationobject orientation

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (17)

Towards imperative modules: reasoning about invariants and sharing of mutable state ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Observational purity and encapsulation ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Towards verification of C\(\#\) programs: a three-level approach ⋮ Confinement framework for encapsulating objects ⋮ Automatic verification of Java programs with dynamic frames ⋮ A Representation-Independent Behavioral Semantics for Object-Oriented Components ⋮ Universe Types for Topology and Encapsulation ⋮ Bestow and atomic: concurrent programming using isolation, delegation and grouping ⋮ CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties ⋮ Unifying separation logic and region logic to allow interoperability ⋮ ProMoVer: Modular Verification of Temporal Safety Properties ⋮ WP Semantics and Behavioral Subtyping ⋮ A proof outline logic for object-oriented programming ⋮ Invariants for Non-Hierarchical Object Structures

Uses Software

• Virginity
• LARCH
• JML

This page was built for publication: Modular specification and verification of object-oriented programs