Détails sur le séminaire


CTL

26 janvier 2012 - 14h00
Quantitative Reactive Modeling
par Tom Henzinger de IST-Austria



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 program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria that include not only function and performance, but also reliability and robustness. For this purpose, we propose quantitative fitness measures for reactive models of concurrent systems. Besides measuring the fit between a system and a requirement numerically, the goal of the project is to obtain quantitative
generalizations of the paradigms on which the success of qualitative reactive modeling rests, such as compositionality, abstraction, model checking, and synthesis.



Special VERIMAG Seminar: Tom Henzinger will obtain a Doctor Honoris Causa title from UJF in 27/1/12

Contact | Plan du site | Site réalisé avec SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4155686