Andreas Podelski:
Verification, Least Fixpoint Checking

Abstract: In this talk we use the framework of abstract least fixpoint checking to explain the formal basis of a range of automatic verification algorithms for properties including termination and for programs including recursive programs. We discuss how decision procedures can be used to increase the degree of automation in these methods.


Bio:
Andreas Podelski has held research positions at the DEC Paris Research Lab and the Max Planck Research Institute before his appointment at the University of Freiburg. His research interests are in program analysis and verification.

Appointments: dcm@cs.cmu.edu


Maintainer Home > Seminar ]
`Last modified: Tues Sep 30 11:09:10 EDT 2008