Abstract

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.