Frame rule for mutually recursive procedures manipulating pointers

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

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)

Cites Work

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

Cited In (3)

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

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)