Compiler-assisted software verification using plug-ins
Sean Callanan, Radu Grosu, Xiaowan Huang, Scott A. Smolka, Erez Zadok · 2006
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 compiletime 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. 1