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