Symbol Elimination for Program Analysis - Laura Kovacs
Workshop on Software Correctness and Reliability 2017
In this talk we describe applications and use of our symbol elimination method in program analysis. We show that symbol elimination adapted to polynomial algebra can automatically infer non-linear program properties, such as loop invariants and loop bounds. By combining techniques from symbolic computation and first-order theorem proving, we then introduce symbol elimination in saturation-based theorem proving and generate first-order program properties, possibly with quantifier alternations, of programs over unbounded data structures.