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

Select |




Print


Tuch, Harvey

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.



Loading citation data...

Citation counts
(Requires subscription to view)