Symbol Elimination in Program Analysis

Talk announcement
HIIT Seminar Kumpula, Friday September 23 10:15, Exactum B222

SPEAKER:
Laura Kovács
Vienna University of Technology

TITLE: 
Symbol Elimination in Program Analysis

ABSTRACT: 
Automatic understanding of the intended meaning of computer
programs is a very hard problem, requiring intelligence and reasoning. 
In this talk we present a new method for program analysis, called 
symbol elimination, that uses first-order theorem proving techniques 
to automatically discover non-trivial program properties, such as 
loop invariants and loop bounds. Moreover, symbol elimination can be 
used as an alternative to interpolation in software verification.

BIO:
Laura Kovács is a Hertha Firnberg Research Fellow of the Austrian Science
Fund at the Institute of Computer Languages of the Vienna University of 
Technology. 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. 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 Wien, she was a postdoctoral
researcher in the Models and Theory of Computation research group of Prof.
Dr. Thomas  A. Henzinger at the Swiss Federal Institute of Technology 
Lausanne (EPFL), and at the Programming Methodology research group of 
Prof. Dr. Peter Müller at the Swiss Federal Institute of Technology 
Zürich (ETH).