Frame rule for mutually recursive procedures manipulating pointers

DOI10.1016/J.TCS.2009.05.016MaRDI QIDQ732009zbMATH OpenOpenAlexFDO

Authors 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

separation logicpointersframe rulemechanical verification of programsmutually recursive procedurespredicate transformer semantics

Mathematics Subject Classification ID

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

Recommendations

• Completeness for recursive procedures in separation logic
• Predicate transformers for recursive procedures with local variables
• Mechanical verification of mutually recursive procedures
• Proof rules for recursive procedures
• scientific article; zbMATH DE number 1500648

Cites work

• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• A proof outline logic for object-oriented programming
• An algebraic treatment of procedure refinement to support mechanical verification
• An axiomatic basis for computer programming
• BI as an assertion language for mutable data structures
• Computer Science Logic
• Higher-order separation logic in Isabelle/HOLCF
• Isabelle/HOL. A proof assistant for higher-order logic
• Refinement Calculus
• Relational Parametricity and Separation Logic

Cited in

(7)

• Completeness for recursive procedures in separation logic
• Algebra of monotonic Boolean transformers
• Algebraic separation logic
• Reasoning about assignments in recursive data structures
• Safe Modification of Pointer Programs in Refinement Calculus
• Verifying object-oriented programs with higher-order separation logic in Coq
• Mechanical verification of mutually recursive procedures

Describes a project that uses

Uses Software

• PVS
• Isabelle/HOL

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q732009)