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

Author:

Tuch, Harvey

Date of Publication:

2009-04-02

Publication Type:

Journal Article

Journal Title:

Journal of Automated Reasoning

Volume:

42

Issue:

2-4

Pages:

125-187

Abstract:

Systems code is almost universally written in the C programming language or a variant. C has a very low level of type and memory abstraction and formal reasoning about C systems code requires a memory model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstraction, in particular from the aliasing and frame problems. In this paper we present a study in the mechanisation of two proof abstractions for pointer program verification in the Isabelle/HOL theorem prover, based on a low-level memory model for C. The language's type system presents challenges for the multiple independent typed heaps (Burstall-Bornat) and separation logic proof techniques. In addition to issues arising from explicit value size/alignment, padding, type-unsafe casts and pointer address arithmetic, structured types such as C's arrays and structs are problematic due to the non-monotonic nature of pointer and lvalue validity in the presence of the unary a working of the standard in-place list reversal example and an overview of the verification of the L4 microkernel's memory allocator.

URL:

http://www.springerlink.com/content/100280/

ISSN/ISBN:

1573-0670

Identifier:

nicta:2324

Attribution Statement:

Tuch, Harvey. Formal verification of C systems code: Structured types, separation logic and theorem proving. Journal of Automated Reasoning. 2009-04-02; 42(2-4):125-187.