From Boolean to Quantitative Methods in Formal Verification

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

• Thomas Henzinger, IST Austria
• Thursday 19 November 2015, 13:00-14:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

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

Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or a program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behaviour of hardware and software in a more nuanced fashion against multiple criteria. We propose quantitative preference metrics for reactive systems, which can be used to measure the degree of desirability of a system with respect to primary attributes such as function and performance, but also with regard to secondary attributes such as robustness and resource consumption. The theory supports quantitative generalizations of the paradigms that have become success stories in boolean formal methods, such as temporal logic, property-preserving abstraction, model checking, and reactive synthesis.

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.