| 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. |
| 2011-12-22 | Our paper "Lazy Abstraction with Interpolation for Arrays" was accepted to LPAR 2012. |
| 2011-09-22 | Our project ''Quality of Interpolants in Model Checking'' has been funded by SNSF for 3 years. The correspondent position for a PhD student is open now. |
| 2011-09-19 | Our paper "Interpolation-based Function Summaries in Bounded Model Checking" was accepted to HVC 2011. |
| 2011-08-30 | Aliaksei Tsitovich received the PhD degree from the University of Lugano, with a thesis titled "Scalable Abstraction for Efficient Security Checks". |
| 2011-06-17 | Prof. Sharygina and Dr. Bruttomesso are presenting OpenSMT and its applications to verification at MIT SAT/SMT summer school. |
| 2011-02-10 | Our article on combination of precise and approximated abstractions appeared in International Journal on Software Tools for Technology Transfer (STTT). |
| 2011-01-03 | Our latest work on the summarization-based termination analysis resulted in the paper, which will be presented at TACAS'11. |
| 2010-12-01 | Our EU project PINCETTE is in the press SwissInfo.ch: "Tweezers to remove errors". |
| 2010-10-18 | Alpine Verification Meeting 2010 in Lugano (see photo) |
| 2010-10-11 | Our EU project PINCETTE is in the press Corriere del Ticino: "Mission: eliminate bugs". |
| 2010-09-01 | The registration for FMCAD 2010 is open. Our Lab will be pleased to welcome you in Lugano on October 20-23, 2010. |
| 2010-08-22 | Our paper "An Efficient and Flexible Approach to Resolution Proof Reduction" was accepted to HVC 2010. |
| 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. |
Formal Verification at University of Lugano
Our Lab is a part of Informatics Faculty at University of Lugano. The 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.
For questions about the Lab projects and open positions, contact natasha [dot] sharygina [at] usi [dot] ch.
We also lead student semestral projects, take a look at the list of topics that we offer.
Read about our Lab in the press.
Latest news
The Lab is funded by Swiss National Science Foundation, Foundation Tasso, Hasler Foundation, EU-COST initiative and EU FP7/Pincette.
