The role of termination in program verification
Registration form: Register here
Course summary:Understanding how to prove the correctness of a program is an essential ingredient in a software engineer's toolbox. A common theme in these proofs involves termination. In this course, I will start with basic concepts of proving algorithms and lead into proof writing. Termination proofs arise for loops, for recursive routines, and for proofs themselves, and we’ll see that these use the same underlying mathematical mechanisms. The lectures and assignments will use Dafny (dafny.org) as the programming language, proof language, and automated verifier.
About the lecturer:K. Rustan M. Leino is known for his work on programming languages and programming methods and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.
He is an ACM Fellow, an IFIP Fellow, and a recipient of the CAV Award.
Leino has been Senior Principal Applied Scientist at Amazon Web Services, Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and researcher at DEC/Compaq Systems Research Center (SRC). He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft.
Location and schedule:
|
|
|
||||||||||||||||