Assertion Checking Environment (ACE) for formal verification of C programs

Abstract

In this paper we describe an Assertion Checking Environment(ACE) for compositional verification of programs which are written in an industrially sponsored safe sub-set of C programming language called MISRA C [1]. The theory is based on Hoare logic [2] and the C programs are verified using static assertion checking technique. First the functional specifications of the program, captured in the form of preand post-conditions for each C function, are derived from the specifications. These pre- and post-conditions are then introduced as assertions(annotations or formal comments) in the program code. The assertions are then proved formally using ACE and theorem proving tool called Stanford Temporal Prover(STeP) [3]. ACE has been developed by us and consists of a translator c2spl, a GUI and some utility programs. The technique and tools developed are targeted towards verification of embedded software.