Section: Overall Objectives

Overall Objectives

Computer systems play a central role in modern societies and their errors can have dramatic consequences. Industry and academics thus invest a considerable amount of effort developing techniques to prove the correctness of these systems. Among such techniques, one finds (1) testing, the traditional approach to detect bugs with test cases, and (2) formal methods, e.g., model checking (Turing award), that can guarantee the absence of bugs. Both approaches have been largely deployed on static systems, whose behaviour is entirely known. ESTASYS focuses on developping brand new formal methods for Systems of Systems.