Formal verification of C systems code: Structured types, separation logic and theorem proving
Tuch, Harvey
2009-04-02
Journal Article
Journal of Automated Reasoning
42
2-4
125-187
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.
http://www.springerlink.com/content/100280/
1573-0670
nicta:2324
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.http://hdl.handle.net/102.100.100/111168?index=1
Loading citation data...
Citation counts
(Requires subscription to view)