Laboratorio di Verifica Automatica di Sistemi Digitali



LA TORRE SalvatoreResponsabile Scientifico

The main research activity of the members of the laboratory concerns with the area of Formal Methods applied to the Verification and Synthesis of Systems. The laboratory offers seminars, internships and thesis advising for the achievement of the Laurea, Master and PhD degrees in Computer Science. The members of the laboratory maintain collaborative relationships with international research institutions and companies operating in the area of the Information Technology (more details).


  • Cseq, an automatic tool for checking C programs competing with POSIX threads based on sequencing. This tool won the silver medal at SVCOMP-TACAS 2013 for the "concurrency" category, the gold and silver medals at SVCOMP-TACAS 2014-2015-2016 and the silver and bronze medals at SVCOMP-TACAS 2017 (
  • Getafix, a model-checker for Boolean programs based on a fixed-point translation (
  • Graded-CTL Nu-SMV, Nu-SMV model-checker integration module with model-checking with specifications expressed in graded-CTL (



+39 089 96 9319


FSTEC-07P04099 (Edificio F - Stecca 7 - Quarto piano - Stanza n. 99).