An extensible encoding of object-oriented data models in HOL. With an application to IMP++
From MaRDI portal
Publication:1040775
DOI10.1007/s10817-008-9108-3zbMath1191.68619OpenAlexW1584909899MaRDI QIDQ1040775
Achim D. Brucker, Burkhart Wolff
Publication date: 25 November 2009
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-008-9108-3
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Semantics, calculi, and analysis for object-oriented specifications ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ On theorem prover-based testing ⋮ IMP++
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Winskel is (almost) right: Towards a mechanized semantics textbook
- Isabelle/HOL. A proof assistant for higher-order logic
- An introduction to mathematical logic and type theory: To truth through proof.
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- HOLCF = HOL + LCF
- Hoare logic for Java in Isabelle/HOL
- Theoretical Aspects of Computing – ICTAC 2005
- Theorem Proving in Higher Order Logics
- FM 2005: Formal Methods
- FM 2005: Formal Methods
This page was built for publication: An extensible encoding of object-oriented data models in HOL. With an application to IMP++
