Frame rule for mutually recursive procedures manipulating pointers

DOI10.1016/J.TCS.2009.05.016zbMATH Open1187.68120OpenAlexW2027587503MaRDI QIDQ732009FDOQ732009

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

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

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)

Cites Work

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

Cited In (5)

• 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

Uses Software

• Isabelle/HOL
• PVS

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)