Research | Lab of Automatic Verification and Synthesis of Systems

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).

Tools

• 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 (http://sv-comp.sosy-lab.org/).
• Getafix, a model-checker for Boolean programs based on a fixed-point translation (http://www.cs.uiuc.edu/homes/madhu/getafix/)
• Graded-CTL Nu-SMV, Nu-SMV model-checker integration module with model-checking with specifications expressed in graded-CTL (http://gradedctl.di.unisa.it/)

Contacts

Telephone

+39 089 96 9319

Location

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