Formal Verification at University of Lugano

Our Lab is a part of Informatics Faculty at University of LuganoThe 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.

For questions about the Lab projects and open positions, contact

We also lead student semestral projects, take a look at the list of topics that we offer.

We have a NEW open PhD position. For more informations, click here.


Latest news


Our security project has been funded by SNSF for 2 more years.


Results of our work on secure mobile code will be presented at the TOOLS Session of the VSTTE 2008


OpenSMT 0.1 was released to public at SMT2008 competition at CAV 2008


The "Loop Summarization using Abstract Transformers" paper was accepted for ATVA2008.


We organized "USI-CMU Summer School on Dependable Computer Systems".


Edgar left for a 3 month internship at Microsoft research.