|
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
| 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 Verification 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 |
| 2009-08-11 |
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 |
| 2009-08-10 |
OpenSMT version 0.2 was released after participation in SMTCOMP'09. It was the first among open-source solvers in UF, RDL, IDL and LRA categories |
| 2009-08-01 |
We have an open position for a PhD student in the project "Automated Invariant Generation for Efficient Security Checks". |
| 2009-07-26 |
"Loopfrog: A Static Analyzer for ANSI-C Programs" tool paper was accepted to ASE'09 |
| 2009-07-16 |
Our Lab organizes FMCAD 2010 that will take place in Lugano on October 20-23, 2010 |
| 2009-06-30 |
Our project on "Automated Invariant Generation for Efficient Security Checks" was approved for 36 months funding by Hasler Foundation |
| 2009-06-19 |
Our work on "Synergy of Precise and Fast Abstractions" was invited for a talk to SAVCBS'09 |
| 2009-06-16 | |
| 2009-05-26 |
Our Lab participates in the EU COST initiative (48 months) on "Rich-Model Toolkit: An Infrastructure for Reliable Computer" that was just approved |
| 2008-12-10 |
Aliaksei Tsitovich presented his Ph.D. research proposal on "Detection of Security Vulnerabilities by Guided Model Checking" at the ICLP'08 Doctoral Consortium |
| 2008-10-12 |
"The Synergy of Precise and Fast Abstractions for Program Verification" paper was accepted to 24th Annual ACM Symposium on Applied Computing |
| 2008-09-08 |
Our security project has been funded by SNSF for 2 more years |
| 2008-08-27 |
Results of our work on secure mobile code will be presented at the TOOLS Session of the VSTTE 2008 |
| 2008-07-15 |
OpenSMT 1.0 was released to public at SMT2008 competition at CAV 2008 |
| 2008-07-04 |
The "Loop Summarization using Abstract Transformers" paper was accepted for ATVA2008 |
