Formal verification of C systems code. Structured types, separation logic and theorem proving
type: Item
instance of: scholarly article
title: Formal verification of C systems code. Structured types, separation logic and theorem proving
zbMATH Open document ID: 1191.68417
author: Harvey Tuch
published in: Journal of Automated Reasoning
publication date: 2009-08-31T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5600119
zbMATH Keywords: separation logic
zbMATH Keywords: C
zbMATH Keywords: interactive theorem proving
describes a project that uses: cminor
describes a project that uses: BLAST
describes a project that uses: Isabelle/HOL
describes a project that uses: CIL
MaRDI profile type: Publication
full work available at URL: s10817-009-9120-2
OpenAlex ID: W1533238174
cites work: Separation Logic for Small-Step cminor
cites work: Q4531754
cites work: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
cites work: Calculating with pointers
cites work: Q2721096
cites work: Q5674963
cites work: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
cites work: Q4474211
cites work: The logic of aliasing
cites work: Theorem Proving in Higher Order Logics
cites work: Q4426387
cites work: BI as an assertion language for mutable data structures
cites work: Q3996398
cites work: Verified bytecode subroutines
cites work: Formal verification of a C-like memory model and its uses for verifying program transformations
cites work: Proving pointer programs in higher-order logic
cites work: Q3038594
cites work: Q4738390
cites work: Term rewriting and beyond -- theorem proving in Isabelle
cites work: Q4783297
cites work: The foundation of a generic theorem prover
cites work: Logic for Programming, Artificial Intelligence, and Reasoning
cites work: Types, bytes, and separation logic
cites work: Computer Science Logic
cites work: Q4738240
DOI: 10.1007/S10817-009-9120-2
Recommended article: Formal verification of cP systems using Coq
Recommended article: Towards verification of C programs. C-light language and its formal semantics
Recommended article: Towards verification of C programs: Axiomatic semantics of the C-kernel language
Recommended article: Q5424313
Recommended article: Q3685173
description: scientific article; zbMATH DE number 5600119