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 Lab organizes FMCAD 2010 that will take place in Lugano on October 20-23, 2010.


Our project on "Automated Invariant Generation for Efficient Security Checks" was approved for 36 months funding by Hasler Foundation.


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


Loopfrog 0.6 is now avaliable.


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


Aliaksei Tsitovich presented his Ph.D. research proposal on "Detection of Security Vulnerabilities by Guided Model Checking" at the ICLP'08 Doctoral Consortium


"The Synergy of Precise and Fast Abstractions for Program Verification" paper was accepted to 24th Annual ACM Symposium on Applied Computing.


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.