First-Order Theorem Proving and 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 describe applications of first-order theorem proving in automated program analysis. We give a short introduction in first-order theorem proving and discuss some of the key concepts in automated theorem proving. We also cover more recent topics and features of first-order theorem proving for advanced applications, including theory reasoning, interpolation, consequence elimination, and program analysis. We show that, with the help of a first-order theorem prover, we are able to derive nontrivial program properties that no other method could derive so far. Such properties include, for example, loop invariants, loop bounds, and Craig interpolants. These properties capture the intended meaning of programs and hence are crucial in the formal analysis and verification of computer systems
Biography:
Laura Kovacs is an associated professor at the Chalmers Unversity of Technology. Her research focuses on automated program analysis, in particular by designing new methods based on the combination of symbolic computation and automated reasoning. She is the main developer of the Aligator software tool and the co-developer of the award-winning Vampire theorem prover. Her work has been awarded by the European Research Council (ERC) with an ERC Starting Grant 2014. She is also the recipient of a Wallenberg Academy Fellowship 2014 of the Knut and Alice Wallenberg Foundation, Sweden's largest and most prestigious private investment in young researchers.