Callanan/Grosu/Huang/Smolka/Zadok

Compiler-Assisted Software Verification Using Plug-Ins*

S. Callanan, R. Grosu, X. Huang, S.A. Smolka and E. Zadok

We present Protagoras, a new plug-in architecture for the GNU compiler collection that allows one to modify GCC's internal representation of the program under compilation. We illustrate the utility of Protagoras by presenting plug-ins for both compile-time and runtime software verification and monitoring. In the compile-time case, we have developed plug-ins that interpret the GIMPLE intermediate representation to verify properties statically. In the runtime case, we have developed plug-ins for GCC to perform memory leak detection, array bounds checking, and reference-count access monitoring.

In Proc. of NGS'06, the Next Generation Software Workshop at IPDPS, April, 2006, Rhodes Island, Greece.

* This work was partially supported by the NSF Faculty Early Career Development Award CCR01-33583 and the NSF CSR-AES05-09230 Award.