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. |
Formal Verification and Security Lab
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
2024-05-14 |
Our paper SolTG: A CHC-based Solidity Test Case Generator has been accepted to CAV 2024 |
2023-11-13 |
Rodrigo Otoni defended his PhD thesis "Automated Verification of Blockchain Technologies with Correctness Guarantees" (09.10.2023) |
2023-10-24 |
Our paper Picky CDCL: SMT-solving With Flexible Literal Selection has been accepted to VSTTE 2023 |
2023-09-08 |
Our paper The Golem CHC Solver was honored with distinguished paper award at CAV 2023 |
2023-09-08 |
Our tool OpenSMT won QF_Equality+LinearArith and QF_LinearRealArith divisions in SMT-COMP 2023. It also won in some of the logics (QF_LIA, QF_LRA, QF_UFIDL). |