_

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-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

Loopfrog 0.6 is now avaliable
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
2008-06-30

We organized "USI-CMU Summer School on Dependable Computer Systems"
2008-05-27

Edgar left for a 3 month internship at Microsoft research

Pages