Presentation title

Introduction to MCLab – the Model Checking Lab

Authors

Enrico Tronci, Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Ivano Salvo

Institution(s)

Model Checking Lab, Sapienza University of Rome

Presentation type

Presentation of a research group from one or more scientific institutions

Abstract

MCLab research activity focuses on model checking-based algorithms and tools for the automatic verification and synthesis of mission or safety critical systems such as, e.g., biodevices and most cyberphysical systems.

MCLab is regularly involved with many research projects sponsored by international funding agencies, such as the European Community (EC) and the European Space Agency (ESA) as well as National funding agencies, such as Italian Ministry of University and Research (MIUR), Italian Ministry of Economic Development (MSE), National Research Council (CNR), ENEA, FILAS as well as private companies.

In all such projects, MCLab research focuses on methods and tools for automatic verification and synthesis of safety-critical control systems.

As a result of such research activities, several tools have been implemented. For example: SyLVer (System Level formal Verifier), SyLVaaS (System Level Verification as a Service), QKS (Quantized Kontrol Synthesizer), NashMV (developed together with the University of Texas at Austin), CMurphi (built on top of Stanford University Murphi verifier), FHP-Murphi (Finite Horizon Probabilistic Murphi).

---

Additional material

• Presentation slides: [pdf]

For more details on this presentation please click the button below: