Formal Verification and Security Lab at USI Lugano

Our Lab is a part of the Informatics Faculty at the 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

2021-03-05

Our paper on Theory-Specific Proof Steps Witnessing Correctness of SMT Executions has been accepted to DAC 2021.
2020-10-24

Matteo Marescotti defended his PhD thesis "Parallelization and modeling techniques for scalable SMT-based verification" (05.10.2020).
2020-09-21

Our paper on Farkas-Based Tree Interpolation has been accepted to SAS 2020.
2020-07-17

Our paper on Incremental Verification by SMT-based Summary Repair has been accepted to FMCAD 2020.
2020-07-10

Our SMT-solver OpenSMT won the QF_LRA Single Query Track of the SMT competition 2020
2020-07-10

Our paper Accurate Smart Contract Verification through Direct Modelling has been accepted to ISoLA 2020
2020-02-03

Our paper A Cooperative Parallelization Approach for Property-Directed k-Induction has been accepted to VMCAI 2020
2019-03-26

Our work was mentioned in the media. (see Microsoft Research blog)
2019-03-24

Our paper SMTS: Distributed, Visualized Constraint Solving has been accepted to LPAR 2018
2019-03-22

Our paper Decomposing Farkas interpolants has been accepted to TACAS 2019
2018-11-29

Our paper Computing Exact Worst-Case Gas Consumption for Smart Contracts has been accepted to ISoLA 2018.
2018-10-23

Our paper Lookahead-Based SMT Solving has been accepted to LPAR-22.
2018-09-24

Our paper Function Summarization Modulo Theories has been accepted to LPAR 2018.
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.

Pages