_

Our Lab is a part of the Informatics Faculty at the University of LuganoThe Lab was established in 2006 when Prof. Sharygina received 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 contact natasha.sharygina@usi.ch.

We have NEW open PhD and Postdoc positions. For more information, contact natasha.sharygina@usi.ch.

Latest news

2021-06-24

Our paper Lattice-based SMT for program verification has been accepted MEMOCODE 2019

2021-06-24

Our paper Exploiting partial variable assignment in interpolation-based model checking  has been accepted to Formal Methods in System Design 2019

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

Pages