Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic

This publication has 9 references indexed in Scilit:

• A Variable Typed Logic of Effects
  Information and Computation, 1995
• Partial functions and logics: A warning
  Information Processing Letters, 1995
• Reasoning about dynamically evolving process structures
  Formal Aspects of Computing, 1994
• A note on undefined expression values in programming logics
  Information Processing Letters, 1987
• A logic covering undefinedness in program proofs
  Acta Informatica, 1984
• Verifying reachability invariants of linked structures
  Published by Association for Computing Machinery (ACM) ,1983
• Soundness and Completeness of an Axiom System for Program Verification
  SIAM Journal on Computing, 1978
• Proving assertions about programs that manipulate data structures
  Published by Association for Computing Machinery (ACM) ,1975
• An axiomatic definition of the programming language PASCAL
  Acta Informatica, 1973