TY - GEN
T1 - Compiler-assisted software verification using plug-ins
AU - Callanan, Sean
AU - Grosu, Radu
AU - Huang, Xiaowan
AU - Smolka, Scott A.
AU - Zadok, Erez
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/33847132872
U2 - 10.1109/IPDPS.2006.1639579
DO - 10.1109/IPDPS.2006.1639579
M3 - Conference contribution
AN - SCOPUS:33847132872
SN - 1424400546
SN - 9781424400546
T3 - 20th International Parallel and Distributed Processing Symposium, IPDPS 2006
BT - 20th International Parallel and Distributed Processing Symposium, IPDPS 2006
PB - IEEE Computer Society
T2 - 20th IEEE International Parallel and Distributed Processing Symposium, IPDPS 2006
Y2 - 25 April 2006 through 29 April 2006
ER -