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
2012-10-24 |
We are co-organizing CAV 2013 |
2012-07-13 |
Our paper "Incremental Upgrade Checking by Means of Interpolation-based Function Summaries" has been accepted to FMCAD 2012 |
2012-07-01 |
The EU FP7/PINCETTE project got the highest possible score from the annual review performed in Brussels in June. The overall assessment states that the progress in the project has been excellent, and that the project has fully achieved its objectives and technical goals for the period and has even exceeded expectations |
2012-06-18 |
Our paper "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization" has been accepted to ATVA 2012 |
2012-03-22 |
Our papers "Leveraging Interpolant Strength in Model Checking" and "SAFARI: SMT-based Abstraction For Arrays with Interpolants" have been accepted to CAV 2012 |