University of Cambridge > > Microsoft Research Cambridge, public talks > From Boolean to Quantitative Methods in Formal Verification

From Boolean to Quantitative Methods in Formal Verification

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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