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

2014-11-19

The MIT-licensed SMT solver OpenSMT2 developed at USI verification group made its debute in the Vienna Summer of Logic 2014 SMT solver competition!
2014-09-22

Our paper "Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection" has been accepted to SBMF 2014.
2014-06-18

Our paper "An extension of lazy abstraction with interpolation for programs with arrays" was published in Formal Methods and System Design.
2014-06-18

Our paper "VERIGE: Verification with Invariant Generation Engine" has been accepted to SPIN 2014.
2014-06-13

Simone Rollini successfully defended his doctoral thesis
2014-02-08

Our paper "Decision Procedures for Flat Array Properties" has been accepted to TACAS 2014.
2014-02-06

Our paper "Incremental Verification of Compiler Optimizations" was accepted to NFM 2014.
2013-09-27

Our paper "PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification" was accepted to LPAR'13.
2013-06-23

Our paper "Loop summarization using state and transition invariants" was published in Formal Methods and System Design 42.
2013-06-20

Our paper "A Parametric Interpolation Framework for First-Order Theories" has been accepted to MICAI 2013.
2013-06-05

Our paper "Interpolation Properties and SAT-Based Model Checking" has been accepted to ATVA 2013.
2013-03-25

Our paper "eVolCheck: Incremental Upgrade Checker for C" has won the best student paper award at TACAS 2013.
2013-03-09

Our paper "PINCETTE - Validating Changes and Upgrades in Networked Software", co-authored with the PINCETTE partners, has won the best paper award at the European Project Track at CSMR 2013.
2013-02-25

Our paper "Interpolation-based mode checking for efficient incremental analysis" was accepted to DDECS 2013.
2013-02-04

Our paper "Definability of Accelerated Relations in a Theory of Arrays and Its Applications" was accepted to FroCoS 13.
2012-11-09

Our paper "Using Cross-Entropy for Satisfiability" has been accepted to SAC 2013.
2012-10-24

We are co-organizing CAV 2013.
2012-07-13

Our paper "Incremental Upgrade Checking by Means of Interpolation-based Function Summaries" has been accepted to FMCAD 2012.
2012-07-01

The EU FP7/PINCETTE project got the highest possible score from the annual review performed in Brussels in June. The overall assessment states that the progress in the project has been excellent, and that the project has fully achieved its objectives and technical goals for the period and has even exceeded expectations.
2012-06-18

Our paper "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization" has been accepted to ATVA 2012.
2012-03-22

Our papers "Leveraging Interpolant Strength in Model Checking" and "SAFARI: SMT-based Abstraction For Arrays with Interpolants" have been accepted to CAV 2012.
2011-12-22

Our paper "Lazy Abstraction with Interpolation for Arrays" was accepted to LPAR 2012.
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".

Pages