| 2010-07-19 | OpenSMT 1.0 alpha has won 3 categories in SMT Competition 2010: QF_IDL, QF_RDL and QF_UFIDL. |
| 2010-06-29 | Our paper "Flexible Interpolation with Local Proof Transformations" was accepted to ICCAD 2010. |
| 2010-05-01 | New paper "A Model Checking-based Approach for Security Policy Veriļ¬cation of Mobile Systems" will appear in the Formal Aspects of Computing Journal. |
| 2010-04-30 | "A Flexible Schema for Generating Explanations in Lazy Theory Propagation" paper was accepted to Memocode 2010. |
| 2010-04-29 | Loopfrog was accepted for a tool session of Workshop on Invariant Generation at FLOC 2010 |
| 2010-03-15 | A paper "Termination Analysis with Compositional Transition Invariants" was accepted to CAV 2010. |
| 2010-03-01 | "PINCETTE" project on Validation of System Upgrades was approved by EU FP7 STREP for 36 months funding. |
| 2010-02-01 | New paper titled "The OpenSMT Solver" will appear at TACAS 2010. |
| 2010-01-15 | New tool for termination analysis of C programs is available. |
| 2009-11-02 | New paper published: A Scalable Decision Procedure for Fixed-Width Bit-Vectors at ICCAD 2009. |
Formal Verification at University of Lugano
Our Lab was established in 2006 when Prof. Sharygina moved from Carnegie Mellon University to University of Lugano after receiving 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.
The Lab is a part of Informatics Faculty at University of Lugano
For questions about the Lab projects and open positions, contact natasha [dot] sharygina [at] usi [dot] ch
Latest news
The Lab is funded by Swiss National Science Foundation, Foundation Tasso, Hasler Foundation, EU-COST initiative and EU FP7.
