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 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-09-01

The registration for FMCAD 2010 is open. Our Lab will be pleased to welcome you in Lugano on October 20-23, 2010.

2010-08-22

Our paper "An Efficient and Flexible Approach to Resolution Proof Reduction" was accepted to HVC 2010.

2010-07-19

OpenSMT 1.0 alpha has won 3 categories in SMT Competition 2010: QF_IDL, QF_RDL and QF_UFIDL.

2010-06-29

Our paper "Flexible Interpolation with Local Proof Transformations" was accepted to ICCAD 2010.

2010-05-01

New paper "A Model Checking-based Approach for Security Policy Verification of Mobile Systems" will appear in the Formal Aspects of Computing Journal.

2010-04-30

"A Flexible Schema for Generating Explanations in Lazy Theory Propagation" paper was accepted to Memocode 2010.

2010-04-29

Loopfrog was accepted for a tool session of Workshop on Invariant Generation at FLOC 2010

2010-03-15

A paper "Termination Analysis with Compositional Transition Invariants" was accepted to CAV 2010.

2010-03-01

"PINCETTE" project on  Validation of System Upgrades was approved by EU FP7 STREP for 36 months funding.

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

Pages