University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Well-founded functions, induction, and extreme predicates in an SMT-based verifier

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2018 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity