Laura Kovács: Symbol elimination for program analysis
Time: Mon 2015-05-18 12.00
Location: Room 4523, Lindstedtsvägen 5, KTH CSC
Participating: Laura Kovács, Chalmers University of Technology
Practicalities
Lunch is served at 12:00 noon (register at this doodle at the latest on Saturday May 16). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.
Abstract
Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this talk we describe applications of our symbol elimination methods in automated program analysis. Symbol elimination uses first-order theorem proving techniques in conjunction with symbolic computation methods, and derives non-trivial program properties, such as loop invariants and loop bounds, in a fully automatic way. Moreover, symbol elimination can be used as an alternative to interpolation for software verification.