Formal Verification at University of Lugano

Our Lab is a part of Informatics Faculty at University of Lugano. The 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 natasha.sharygina@usi.ch.

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

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 months 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.
2008-12-10

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

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

Our security project has been funded by SNSF for 2 more years.
2008-08-27

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

OpenSMT 0.1 was released to public at SMT2008 competition at CAV 2008
2008-07-04

The "Loop Summarization using Abstract Transformers" paper was accepted for ATVA2008.
2008-06-30

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

Edgar left for a 3 month internship at Microsoft research.

Pages