Specification and verification challenges for sequential object-oriented programs

DOI10.1007/s00165-007-0026-7zbMath1121.68074MaRDI QIDQ2643131

Peter Müller, K. Rustan M. Leino, Gary T. Leavens

Publication date: 23 August 2007

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://lib.dr.iastate.edu/cs_techreports/340

zbMATH Keywords

Specification; Object-oriented programming; Contract; Program verification

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

A Machine Checked Soundness Proof for an Intermediate Verification Language

Uses Software

• Cogent
• LARCH
• SPARK
• KRAKATOA
• Haskell
• Eiffel
• Daikon
• JML
• Spec#
• Omnibus
• SIMPLIFY
• ESC/Java
• Boogie
• CalcCheck
• Z
• Houdini
• ANNA

Cites Work

• Final algebra semantics and data type extensions
• Partial abstract types
• How the design of JML accommodates both runtime assertion checking and formal verification
• Program logic and equivalence in the presence of garbage collection.
• Weakest pre-condition reasoning for Java programs with JML annotations
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Specification and verification of object-oriented programs using supertype abstraction
• Modular invariants for layered object structures
• Proof of correctness of data representations
• Correct and Robust Programs
• Simplify: a theorem prover for program checking
• Writing Larch interface language specifications
• Ten Years of Hoare's Logic: A Survey—Part I
• Initial Algebra Semantics and Continuous Algebras
• The B-Book
• Hoare logic for Java in Isabelle/HOL
• Modular specification of frame properties in JML
• Separation logic and abstraction
• Scalable error detection using boolean satisfiability
• Formal Specification and Design
• Mathematics of Program Construction
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Computer Aided Verification
• Modular specification and verification of object-oriented programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item