Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Rustan Leino

LFCS Seminar: Rustan Leino

— filed under:

Building an SMT-based program verifier using Boogie

  • LFCS Seminar
When May 05, 2011
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Contact Name
Add event to calendar vCal

In this talk, I will cover some topics on how to make use of the Boogie intermediate verification language when building a program analyzer or program verifier. Among these topics are modeling memory, not letting recursive functions get out of hand, and incorporating a simple and effective induction tactic.

Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research in Redmond. His research interests include a focus on programming tools, both mental and mechanical. He is known for his work on automated program verification, leading the development of tools like Spec# and ESC/Java to support specifying and checking object-oriented code within integrated development environments.

On Wednesday afternoon, Dr Leino will be giving the Informatics Distinguished Lecture. If you are interested in meeting with him during his stay in Edinburgh, please email

Links: Distinguished Lecture;Rustan Leino; Research in Software Engineering; Microsoft Research.
Document Actions