Go to the University of Bologna homepage
Department of Electrical, Electronic, and Information Engineering "Guglielmo Marconi" - DEI

Seminar: From Formal Verification to Model-Based Safety Analysis

The seminar will be given by Dr. Alessandro Cimatti, Fondazione Kessler, Italy, as part of the course on "Design for Testability and Reliability of Integrated Circuits M".

  • Date: 13 May 2015 from 14:00 to 16:00

  • Event location: Room 2.7, School of Engineering and Architecture, viale Risorgimento 2, Bologna

Contact Name:

Contact Phone: +39 051 20 93013

Abstract

Model checking is an automated formal verification technique, that is able to prove that a transition system satisfies a given property, or to produce a simulation trace witnessing the violation. Advanced symbolic techniques such as Binary Decision Diagrams and Satisfiability Modulo Theories support the exhaustive exploration of enormous or infinite state spaces. Initially developed for the design of communication protocols and hardware designs, model checking has then been applied to the design of microcode, system level designs, and railways and aerospace. In this talk I will first overview the field of model checking. Then, I will present how model checking has been extended to analyze the impact of faults on complex systems, to automate the construction of Fault Trees, and to characterize the reliability of architectures based on redundancy.

About the speaker

Alessandro Cimatti is a senior researcher at Fondazione Bruno Kessler, Trento, Italy, where he leads the research unit in Embedded Systems at the Center for Information and Communication Technologies. His research interests concern formal verification of industrial critical systems, methodologies for design and verification of hardware/software systems, decision procedures and their application, safety analysis, diagnosis and diagnosability. Cimatti has published more than one hundred and thirty papers in the fields of Formal Methods and Artificial Intelligence. He has co-chaired the FMCAD and SAT conferences, and has been member of the Program Committee of the major conferences in computer-aided verification and artificial intelligence. Cimatti is also interested in the development of software tools for verification (including the MathSAT SMT solver and the NuSMV model checker), and in their application on the field. Cimatti has been the leader of several technology transfer projects in related fields, including projects funded by the European Space Agency, the European Railways Agency, Ansaldo and Boeing.