Program Analysis and Symbol Elimination

Speaker  Laura Kovács

Host  Nikolaj Bjorner

Affiliation  Vienna University of Technology

Duration  01:21:00

Date recorded  26 February 2013

In this talk we describe how the combination of automated reasoning and symbolic computation methods can be used to automatically generate statements expressing arbitrarily complex computer program properties. The common method of the the talk is our recently introduced symbol elimination method. The approach requires no preliminary knowledge about program behavior, uses the power of a theorem prover and/or symbolic computation algorithms, such as Groebner basis computation, and infers quantified loop invariants and interpolants. We will also present recent developments of symbol elimination in the Vampire theorem prover.

©2013 Microsoft Corporation. All rights reserved.
> Program Analysis and Symbol Elimination