Symbol Elimination for Program Analysis

ABSTRACT. In this talk I describe how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the logically complex parts of software. I will first present how computer algebra methods, such as Groebner basis computation and symbolic summation help us in inferring properties of program loops with non-trivial arithmetic. I will then further extend our work to generate first-order properties of programs with unbounded data structures, such as arrays. For doing so, I will use saturation-based first-order theorem proving and extend first-order provers with support for program analysis. I will review some of our recent results on Craig interpolation and proving properties in the full first-order theories of data structures. Our work is implemented in the Vampire theorem prover and successfully applied on benchmarks from the software verification and automated reasoning communities.

Authors

• Laura Kovács

Keywords

No keywords are indexed for this paper.