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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

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

Download to your calendar using vCal

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

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:

Note that ex-directory lists are not shown.

Other lists

room 187, British Antarctic Survey, High Cross, Cambridge, CB3 0ET INI Seminar Room 1 Edwards Room, Bragg building, Cavendish Laboratory

Other talks

title abstract tba TOWARD AFFORDABLE PREVENTIVE HEALTHCARE: How basic science addresses grand challenges Spectral theory for Dirac operators with singular potentials Whether and when: Split-population cure models of women's work and parity progression in Derbyshire, 1881-1911 Fairy Tales Washing machines and their rare components: lessons from kidney patients
 

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