Program Analysis and Symbol Elimination

  • Laura Kovács | Vienna University of Technology

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.

登壇者詳細

Laura Kovács is an Hertha Firnberg Research Fellow of the Austrian Science Fund
and an Assistant Professor at the Vienna University of Technology – TU Vienna.
Her research deals with the design and development of new theories, technologies,
and tools for program verification, with a particular focus on automated assertion
generation, symbolic summation, computer algebra, and automated theorem proving.
Together with 8 other researchers, she is founding member of the Austrian Society
for Rigorous Systems Engineering – ARiSE. She holds an MSc from the
Western University of Timisoara, Romania, and a PhD degree from the
Research Institute for Symbolic Computation of the Johannes Kepler University,
Linz, Austria. Before joining TU Vienna, she was a postdoctoral researcher
at the Swiss Federal Institutes of Technology Lausanne (EPFL) and Zürich (ETH).

シリーズ: Microsoft Research Talks