Hoare logic for Java in Isabelle/HOL

DOI10.1002/CPE.598MaRDI QIDQ4329634zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

Java CardHoare-style calculus

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• scientific article; zbMATH DE number 2110621
• scientific article; zbMATH DE number 2090132
• A syntax-directed Hoare logic for object-oriented programming concepts.
• Algebraic Methodology and Software Technology
• A sound and complete Hoare logic for dynamically-typed, object-oriented programs

Cites work

• scientific article; zbMATH DE number 1670748 (Why is no real title available?)
• scientific article; zbMATH DE number 986407 (Why is no real title available?)
• scientific article; zbMATH DE number 1251179 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A formulation of the simple theory of types
• An axiomatic basis for computer programming
• Axiomatic approach to side effects and general jumps
• Edinburgh LCF. A mechanized logic of computation
• Fundamental concepts in programming languages
• Isabelle. A generic theorem prover
• Modular specification and verification of object-oriented programs
• Side effects and aliasing can have simple axiomatic descriptions
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(29)

• scientific article; zbMATH DE number 2090132 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 1693528 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 1693527 (Why is no real title available?)
• 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++
• \(\mu\)Java: Embedding a programming language in a theorem prover
• Reasoning about resources in the embedded systems language Hume
• 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
• Computing Preconditions and Postconditions of While Loops
• Formal Methods for Components and Objects

Describes a project that uses

Uses Software

• JML
• Isabelle/HOL
• Isabelle

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)