Proving pointer programs in higher-order logic
From MaRDI portal
Publication:2486585
DOI10.1016/j.ic.2004.10.007zbMath1081.68008OpenAlexW2011270512MaRDI QIDQ2486585
Publication date: 5 August 2005
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2004.10.007
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Formal verification of C systems code. Structured types, separation logic and theorem proving, Practical Tactics for Separation Logic, Convergence: integrating termination and abort-freedom, A Program Construction and Verification Tool for Separation Logic, Inter-process buffers in separation logic with rely-guarantee, Reasoning about memory layouts, Invariant diagrams with data refinement, Certifying assembly with formal security proofs: the case of BBS, Lightweight Separation, Data Refinement of Invariant Based Programs, Formal study of functional orbits in finite domains, Reasoning about Assignments in Recursive Data Structures, Verification of the Schorr-Waite Algorithm – From Trees to Graphs, Formal verification of a C-like memory model and its uses for verifying program transformations, Juggrnaut: using graph grammars for abstracting unbounded heap structures, A Machine-Checked Framework for Relational Separation Logic
Uses Software
Cites Work
- Winskel is (almost) right: Towards a mechanized semantics textbook
- Isabelle/HOL. A proof assistant for higher-order logic
- Click’n Prove: Interactive Proofs within Set Theory
- An efficient machine-independent procedure for garbage collection in various list structures
- Automated Deduction – CADE-19
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
