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

2011-09-22

Our project ''Quality of Interpolants in Model Checking'' has been funded by SNSF for 3 years. The correspondent position for a PhD student is open now.

2011-09-19

Our paper "Interpolation-based Function Summaries in Bounded Model Checking" was accepted to HVC 2011.

2011-08-30

Aliaksei Tsitovich received the PhD degree from the University of Lugano, with a thesis titled "Scalable Abstraction for Efficient Security Checks".

2011-06-17

Prof. Sharygina and Dr. Bruttomesso are presenting OpenSMT and its applications to verification at MIT SAT/SMT summer school.

2011-02-10

Our article on combination of precise and approximated abstractions appeared in  International Journal on Software Tools for Technology Transfer (STTT).

2011-01-03

Our latest work on the summarization-based termination analysis resulted in the paper, which will be presented atTACAS'11.

2010-12-01

Our EU project PINCETTE is in the press SwissInfo.ch: "Tweezers to remove errors".

2010-10-18

Alpine Verification Meeting 2010 in Lugano (see photo)

2010-10-11

Our EU project PINCETTE is in the press Corriere del Ticino: "Mission: eliminate bugs".

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

Pages