Proving pointer programs in Hoare logic

DOI10.1007/10722010_8MaRDI QIDQ2721096zbMATH OpenFDO

Authors Richard Bornat

Publication date 1 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10722010_8

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proving pointer programs in higher-order logic
• Proving pointer programs in higher-order logic.
• Pointer logic for verification of pointer programs
• Local reasoning about programs that alter data structures
• Automata, Languages and Programming

Cited in

(39)

• Operating system verification---an overview
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Correctness of data representations involving heap data structures
• On building cyclic and shared structures in Haskell
• Verifying Whiley programs with Boogie
• Region analysis for deductive verification of C programs
• Analysis of correct synchronization of operating system components
• A program logic for resources
• Verification of finite iterations over collections of variable data structures
• Proving pointer programs in higher-order logic
• Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures
• Laws of programming for references
• Reasoning about assignments in recursive data structures
• Verification of the Schorr-Waite algorithm -- from trees to graphs
• Pointer logic for verification of pointer programs
• A machine-checked framework for relational separation logic
• scientific article; zbMATH DE number 3845029 (Why is no real title available?)
• Safe Modification of Pointer Programs in Refinement Calculus
• Lightweight Separation
• Compositional Reasoning for Pointer Structures
• Verification conditions for source-level imperative programs
• Local reasoning about programs that alter data structures
• Formal study of functional orbits in finite domains
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Heaps and Data Structures: A Challenge for Automated Provers
• Reasoning about separation using abstraction and reification
• Mathematics of Program Construction
• Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
• Static Analysis
• Proving pointer programs in higher-order logic.
• Blaming the client: on data refinement in the presence of pointers
• Inter-process buffers in separation logic with rely-guarantee
• An algebraic glimpse at bunched implications and separation logic
• Doomed program points
• Reasoning about memory layouts
• Formalization of Refinement Calculus for Reactive Systems
• Algebra of Monotonic Boolean Transformers
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Formal verification of a C-like memory model and its uses for verifying program transformations

This page was built for publication: Proving pointer programs in Hoare logic

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