Frame rule for mutually recursive procedures manipulating pointers

DOI10.1016/J.TCS.2009.05.016zbMath1187.68120OpenAlexW2027587503MaRDI QIDQ732009

Viorel Preoteasa

Publication date: 9 October 2009

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2009.05.016

zbMATH Keywords

predicate transformer semanticsseparation logicpointersframe rulemechanical verification of programsmutually recursive procedures

Mathematics Subject Classification ID

Theory of programming languages (68N15) General topics in the theory of software (68N01)

Related Items (3)

Algebraic separation logic ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq ⋮ Algebra of Monotonic Boolean Transformers

Uses Software

• Isabelle/HOL
• PVS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• A proof outline logic for object-oriented programming
• An algebraic treatment of procedure refinement to support mechanical verification
• A lattice-theoretical fixpoint theorem and its applications
• Relational Parametricity and Separation Logic
• Refinement Calculus
• BI as an assertion language for mutable data structures
• Computer Science Logic
• Higher-Order Separation Logic in Isabelle/HOLCF
• An axiomatic basis for computer programming

This page was built for publication: Frame rule for mutually recursive procedures manipulating pointers