Formal verification of C systems code. Structured types, separation logic and theorem proving

DOI10.1007/s10817-009-9120-2zbMath1191.68417OpenAlexW1533238174MaRDI QIDQ835768

Harvey Tuch

Publication date: 31 August 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9120-2

zbMATH Keywords

separation logicinteractive theorem provingC

Mathematics Subject Classification ID

Related Items (2)

Types, Maps and Separation Logic ⋮ Lightweight Separation

Uses Software

• Isabelle/HOL
• BLAST
• cminor
• CIL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Term rewriting and beyond -- theorem proving in Isabelle
• Formal verification of a C-like memory model and its uses for verifying program transformations
• The logic of aliasing
• Verified bytecode subroutines
• Calculating with pointers
• The foundation of a generic theorem prover
• Proving pointer programs in higher-order logic
• Types, bytes, and separation logic
• Separation Logic for Small-Step cminor
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• BI as an assertion language for mutable data structures
• Computer Science Logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Theorem Proving in Higher Order Logics
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Formal verification of C systems code. Structured types, separation logic and theorem proving