Well-founded functions, induction, and extreme predicates in an SMT-based verifier

Add to your list(s) Download to your calendar using vCal

• Rustan Leino, Microsoft Research Redmond
• Thursday 01 December 2016, 10:00-11:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact lecturescam.

Please note, this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

An SMT solver takes first-order formulas as input and provides impressive automation. But what if the problem at hand goes beyond first order? The Dafny program verifier provides well-functions, inductive proofs, and predicates defined as least and greatest fixpoints. It encodes properties of these into first-order logic in such a way that harnesses the automation of SMT solvers. In this talk, I will give an overview of functions and induction in Dafny, and will then focus on the encoding on predicates defined by fixpoints. I hope to learn more about fixpoints and ordinal numbers as I do.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.