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.
We have NEW open PhD and Postdoc positions. For more information, contact firstname.lastname@example.org.
OpenSMT 1.0 alpha has won 3 categories in SMT Competition 2010: QF_IDL, QF_RDL and QF_UFIDL
Our paper "Flexible Interpolation with Local Proof Transformations" was accepted to ICCAD 2010
New paper "A Model Checking-based Approach for Security Policy Veriﬁcation of Mobile Systems" will appear in the Formal Aspects of Computing Journal
"A Flexible Schema for Generating Explanations in Lazy Theory Propagation" paper was accepted to Memocode 2010
A paper "Termination Analysis with Compositional Transition Invariants" was accepted to CAV 2010
"PINCETTE" project on Validation of System Upgrades was approved by EU FP7 STREP for 36 months funding
New tool for termination analysis of C programs is available
New paper published: A Scalable Decision Procedure for Fixed-Width Bit-Vectors at ICCAD 2009
The recent results on OpenSMT (plus an OpenSMT tool description) were presented at SMT'09. More information can found at ie.technion.ac.il/SMT09
We have an open position for a PhD student in the project "Automated Invariant Generation for Efficient Security Checks".
Our Lab organizes FMCAD 2010 that will take place in Lugano on October 20-23, 2010
Our project on "Automated Invariant Generation for Efficient Security Checks" was approved for 36 months funding by Hasler Foundation
Our Lab participates in the EU COST initiative (48 months) on "Rich-Model Toolkit: An Infrastructure for Reliable Computer" that was just approved
Aliaksei Tsitovich presented his Ph.D. research proposal on "Detection of Security Vulnerabilities by Guided Model Checking" at the ICLP'08 Doctoral Consortium