Hoare logic for Java in Isabelle/HOL
- 13 November 2001
- journal article
- research article
- Published by Wiley in Concurrency and Computation: Practice and Experience
- Vol. 13 (13) , 1173-1214
- https://doi.org/10.1002/cpe.598
Abstract
No abstract availableKeywords
This publication has 24 references indexed in Scilit:
- Java Program Verification via a Hoare Logic with Abrupt TerminationPublished by Springer Nature ,2000
- Implementing a Program Logic of Objects in a Higher-Order Logic Theorem ProverPublished by Springer Nature ,2000
- A mechanically verified verification condition generatorThe Computer Journal, 1995
- Side effects and aliasing can have simple axiomatic descriptionsACM Transactions on Programming Languages and Systems, 1985
- Ten Years of Hoare's Logic: A Survey—Part IACM Transactions on Programming Languages and Systems, 1981
- Soundness and Completeness of an Axiom System for Program VerificationSIAM Journal on Computing, 1978
- Axiomatic approach to side effects and general jumpsActa Informatica, 1977
- A technique for software module specification with examplesCommunications of the ACM, 1972
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940