The xGCC analysis tool

Werner Backes
Stevens Institute of Technology


Abstract

In this talk, I will present the xGCC analysis tool for the verification of safety properties of the XRTL intermediate language. These properties include the absence of buffer overflow, division by zero and the use of uninitialized variables and memory. XRTL is an extension of the Register Transfer Language (RTL) generated by a modified GCC. Abstract interpretation is used for the analysis of XRTL. We introduce approximation by lists of valid intervals for the abstraction of sets of registers and memory blocks. Branching conditions are taken into account for restricting the search space, and widening/narrowing techniques are used to speed up the fixpoint computation for XRTL loops. If time permits, I will also talk about improvements towards a semi-automatic analysis that was carried out as part of the Stevens Technogenesis Summer Scholars program.