How Formal Verification Improves Software and AI Reliability

• Joost-Pieter Katoen (RWTH Aachen University)

Room: 774/R-013 Formal verification, in particular model checking and formal synthesis, offers a plethora of techniques so as to increase the reliability of software systems. In this talk, I will present some of our efforts to bring formal verification into industrial practice. This includes the development of a comprehensive AADL analysis tool for the European Space Agency, a model checker for Siemens to check their programmable logic controllers, a reliability analysis tool for static and dynamic fault trees, and a competitive probabilistic model checker.