Formal Verification at University of Lugano

Our Lab was established in 2006 when Prof. Sharygina moved from Carnegie Mellon University to University of Lugano after receiving a career award from the Tasso Foundation. The Lab projects focus on automated formal verification with a particular interest in software/hardware model checking, information security, static analysis, abstract interpretation and decision procedures. We create both theoretical frameworks and practical tools to enable sound and scalable verification of industrial-size systems.

The Lab is a part of Informatics Faculty at University of Lugano

For questions about the Lab projects and open positions, contact Prof. Natasha Sharygina

Latest news
2010-02-01

New paper titled "The OpenSMT Solver" will appear at TACAS 2010.
2010-01-15

New tool for termination analysis of C programs is available.
2009-11-02

 New paper published: A Scalable Decision Procedure for Fixed-Width Bit-Vectors at ICCAD 2009.
2009-08-11

The recent results on OpenSMT  (plus an OpenSMT tool description) were presented at SMT'09. More information can found at ie.technion.ac.il/SMT09.
2009-08-10

OpenSMT version 0.2 was released after participation in SMTCOMP'09. It was the first among open-source solvers in UF, RDL, IDL and LRA categories. 
2009-08-01

We have an open position for a PhD student in the project "Automated Invariant Generation for Efficient Security Checks".
2009-07-26

"Loopfrog: A Static Analyzer for ANSI-C Programs" tool paper was accepted to ASE'09
2009-07-16

Our Lab organizes FMCAD 2010 that will take place in Lugano on October 20-23, 2010.
2009-06-30

Our project on "Automated Invariant Generation for Efficient Security Checks" was approved for 36 month funding by Hasler Foundation.
2009-06-19

Our work on "Synergy of Precise and Fast Abstractions" was invited for a talk to SAVCBS'09
2009-06-16

Loopfrog 0.6 is now avaliable.
2009-05-26

Our Lab participates in the EU COST initiative (48 months) on "Rich-Model Toolkit: An Infrastructure for Reliable Computer" that was just approved.