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

2018-08-30

The result of our joint work with King's College London "Lattice-Based Refinement in BMC" has been accepted to VSTTE 2018 .
2017-10-09

Our paper "LRA Interpolants from No Man's Land" has been accepted to HVC 2017.
2017-10-09

Our paper "Duality-based interpolation for quantifier-free equalities and uninterpreted functions" has been accepted to FMCAD 2017.
2017-06-30

Our paper "Theory Refinement for Program Verification" was accepted to the International Conference on Theory and Applications of Satisfiability Testing (SAT '17).
2016-12-23

Our paper "HiFrog: SMT-based Function Summarization for Software Verication" has been accepted to TACAS 2017.
2016-12-22

Leonardo de Sá Alt successfully defended his doctoral thesis "Controlled and Effective Interpolation", 2016-12-09
2016-08-04

Our paper "Clause Sharing and Partitioning for Cloud-Based SMT Solving" was accepted to ATVA 2016.
2016-08-04

Our paper "Flexible Interpolation for Efficient Model Checking" was accepted to MEMICS 2016.
2016-08-04

Our paper "Combining parallel techniques for Cloud-Based SMT Solving" was accepted to PhD-iFM 2016.
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.

Pages