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-09-25 |
Our paper "Reachability Analysis for Multiloop Programs Using Transition Power Abstraction" has been selected as distinguished paper at FM2024. |
2024-09-12 |
OpenSMT's distributed implementation, SMTS, achieved the best results in the experimental parallel and cloud tracks on SMT-COMP 2024 |
2024-09-12 |
OpenSMT participated in SMT-COMP 2024 across all tracks, achieving impressive results. It secured the top scores in the QF_LRA and single query tracks and demonstrated strong performance in the quantifier-free linear arithmetic and equality divisions.
|
2024-07-03 |
Our paper Reachability Analysis for Multiloop Programs Using Transition Power Abstraction has been accepted to FM 2024 |
2024-07-03 |
Our group gave talks about Golem and SolTG projects at LPAR 2024 in Mauritius. |