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

2016-01-11

Our project ''Quality of Interpolants in Model Checking'' has been extended by SNSF for 2 more years.
2016-01-11

Grigory Fedyukovich successfully defended his PhD thesis "Automated Software Incremental Verification".
2015-09-15

Our paper "Automated Discovery of Simulation Between Programs" was accepted to LPAR 2015.
2015-07-01

Our paper "Search-Space Partitioning for Parallelizing SMT Solvers" was accepted to SAT 2015.
2015-07-01

Our paper "A Proof-Sensitive Approach for Small Propositional Interpolants" was accepted to VSTTE 2015.
2015-07-01

Our paper "A new Acceleration-based Combination Framework for Array Properties" was accepted to FROCOS 2015.
2015-05-13

Francesco Alberti's PhD thesis in now published.
2015-04-27

Our paper "Decision Procedures for Flat Array Properties" was published in Journal of Automated Reasoning, Volume 54.
2015-02-01

Our paper "Symbolic Detection of Assertion Dependencies for Bounded Model Checking" has been accepted to FASE 2015.
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.

Pages