BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From Boolean to Quantitative Methods in Formal Verification - Thom
 as Henzinger\, IST Austria
DTSTART:20151119T130000Z
DTEND:20151119T140000Z
UID:TALK62635@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Formal verification aims to improve the quality of hardware an
 d software by detecting errors before they do harm. At the basis of formal
  verification lies the logical notion of correctness\, which purports to c
 apture whether or not a circuit or a program behaves as desired. We sugges
 t that the boolean partition into correct and incorrect systems falls shor
 t of the practical need to assess the behaviour of hardware and software i
 n a more nuanced fashion against multiple criteria. We propose quantitativ
 e preference metrics for reactive systems\, which can be used to measure t
 he degree of desirability of a system with respect to primary attributes s
 uch as function and performance\, but also with regard to secondary attrib
 utes such as robustness and resource consumption. The theory supports quan
 titative 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.\n\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR