Proving pointer programs in higher-order logic.
From MaRDI portal
Recommendations
Cited in
(20)- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- Imperative Functional Programming with Isabelle/HOL
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- A program logic for resources
- Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
- Gale-Shapley verified
- scientific article; zbMATH DE number 1612488 (Why is no real title available?)
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- scientific article; zbMATH DE number 4156407 (Why is no real title available?)
- Higher-order separation logic in Isabelle/HOLCF
- Reasoning about memory layouts
- Pointer logic for verification of pointer programs
- Proving pointer programs in higher-order logic
- A mechanical analysis of program verification strategies
- Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures
- Compositional Reasoning for Pointer Structures
- Programming Languages and Systems
- Dafny: an automatic program verifier for functional correctness
- Verification of the Schorr-Waite algorithm -- from trees to graphs
- scientific article; zbMATH DE number 7649962 (Why is no real title available?)
This page was built for publication: Proving pointer programs in higher-order logic.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5900714)
