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
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! |