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

2016-04-18

Our paper "Property Directed Equivalence via Abstract Simulation" was accepted to CAV 2016.

2016-04-18

Our paper "OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing" was accepted to SAT 2016.

2016-01-12

Our paper "PVAIR: Partial Variable Assignment InterpolatoR" was accepted to FASE 2016.

2016-01-11

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

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'19.

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.

Pages