An Enhanced Assertion Checking Environment for C Programs
This project aims at enhancing ACE, an existing assertion checking environment for C programs. Using ACE one can formally verify single C functions or programs containing a number of C functions. ACE expects all specification to be given by the user. It can not perform certain standard checks like range checking, underflow and overflow errors automatically. It also can not handle C programs with support for concurrency.
The aim of this project is to extend ACE to include these utilities into the environment to verify C programs. ACE uses STeP as the verification engine. The proposed enhancement make use of powerful PVS verification engine, which has support for automatic type checking.

Related Papers
Babita Sharma, S.D. Dhodapkar and S. Ramesh, Assertion Checking Environment(ACE) for Formal Verification of C Programs, Proc. of SAFECOMP 2002, LNCS Vol. 2434, Springer, September 2002.[ps]