Hoare logic for Java in Isabelle/HOL
From MaRDI portal
Publication:4329634
DOI10.1002/CPE.598zbMATH Open0997.68019OpenAlexW1987693120MaRDI QIDQ4329634FDOQ4329634
Authors: David von Oheimb 
Publication date: 14 November 2002
Published in: Concurrency and Computation: Practice and Experience (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1002/cpe.598
Recommendations
Cites Work
- Title not available (Why is that?)
- Edinburgh LCF. A mechanized logic of computation
- Isabelle. A generic theorem prover
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- Fundamental concepts in programming languages
- Ten Years of Hoare's Logic: A Survey—Part I
- Soundness and Completeness of an Axiom System for Program Verification
- A formulation of the simple theory of types
- Axiomatic approach to side effects and general jumps
- Modular specification and verification of object-oriented programs
- Title not available (Why is that?)
- Side effects and aliasing can have simple axiomatic descriptions
- Title not available (Why is that?)
Cited In (29)
- Title not available (Why is that?)
- A generic complete dynamic logic for reasoning about purity and effects
- A UTP approach for rTiMo
- An observationally complete program logic for imperative higher-order functions
- Title not available (Why is that?)
- A program logic for resources
- Verified bytecode verification and type-certifying compilation
- Verification of object-oriented programs: a transformational approach
- Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
- Equational theories of abnormal termination based on Kleene algebra
- Lazy behavioral subtyping
- Integrating ADTs in KeY and their application to history-based reasoning about collection
- Title not available (Why is that?)
- Semantics, calculi, and analysis for object-oriented specifications
- Introduction to ``Milestones in interactive theorem proving
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Verification conditions for source-level imperative programs
- A dynamic logic for deductive verification of multi-threaded programs
- On theorem prover-based testing
- A syntax-directed Hoare logic for object-oriented programming concepts.
- rCOS: a refinement calculus of object systems
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Reasoning about resources in the embedded systems language Hume
- \(\mu\)Java: Embedding a programming language in a theorem prover
- Specification and verification challenges for sequential object-oriented programs
- An assertion-based proof system for multithreaded Java
- A proof outline logic for object-oriented programming
- Formal Methods for Components and Objects
- Computing Preconditions and Postconditions of While Loops
Uses Software
This page was built for publication: Hoare logic for Java in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4329634)
