Programming Research Group

Automated Verification of low-level Pointer Programs

The verification of C programs that manipulate memory through pointers is currently not supported well by automated reasoning techniques. For reasonable support, Burstall's memory model, which prescribes that the only allowable pointers are references to heap-allocated disjoint records, must be adopted. This assumption precludes, however, many idiomatic C programming constructs: pointers to local variables, to fields inside larger structs, or to array slices are frequently passed to functions, but they cannot be formalized.

We have developed the lightweight separation method to overcome these limitations. The method allows arbitrary memory layouts to be defined in such a way that specialized proof procedures can include their properties in the verification of programs.

The next step in the project concerns the transfer to the C++ language. Encapsulation and invariants, as well as the template mechanism, pose orthogonal challenges that need to be integrated with this method.

Contact: Holger Gast

Address

Universität Tübingen

Wilhelm-Schickard-Institut für Informatik

Jasminweg 21

72076 Tübingen

GERMANY