Specification and verification challenges for sequential object-oriented programs
From MaRDI portal
Publication:2643131
DOI10.1007/s00165-007-0026-7zbMath1121.68074OpenAlexW1977978965MaRDI QIDQ2643131
Gary T. Leavens, Peter Müller, K. Rustan M. Leino
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
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (12)
An overview of Ciao and its design philosophy ⋮ Blaming the client: on data refinement in the presence of pointers ⋮ Practical run-time checking via unobtrusive property caching ⋮ JCML: A specification language for the runtime verification of Java card programs ⋮ Verification conditions for source-level imperative programs ⋮ Automatic verification of Java programs with dynamic frames ⋮ Lazy behavioral subtyping ⋮ A Machine Checked Soundness Proof for an Intermediate Verification Language ⋮ Dynamic Frames in Java Dynamic Logic ⋮ A Refinement Methodology for Object-Oriented Programs ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification
Uses Software
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
This page was built for publication: Specification and verification challenges for sequential object-oriented programs
