Skip to main content

Unrestricted Procedure Calls in Hoare's Logic

Robert Cartwright, Derek C. Oppen

PDF DOI 10.1145/512760.512774 dblp BibTeX

Abstract

This paper presents a new version of Hoare's logic including generalized procedure call and assignment rules which correctly handle aliased variables. Formal justifications are given for the new rules.

Related papers

Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic TOPLAS 2021
Assignment and Procedure Call Proof Rules TOPLAS 1980
A Good Hoare Axiom System for an Algol-like Language POPL 1984
Ten Years of Hoare's Logic: A Survey - Part 1 TOPLAS 1981
Crowfoot: A Verifier for Higher-Order Store Programs VMCAI 2012
Complexity and information in invariant inference POPL 2020
Compositional shape analysis by means of bi-abduction POPL 2009
Bottom-up shape analysis using LISF TOPLAS 2011