Our paper "Definability of Accelerated Relations in a Theory of Arrays and its Applications" has been accepted to FroCoS 2013.
Our paper "eVolCheck: Incremental Upgrade Checker for C" has won the best student paper award at TACAS 2013.
Our paper "PINCETTE - Validating Changes and Upgrades in Networked Software", co-authored with the PINCETTE partners, has won the best paper award at the European Project Track at CSMR 2013.
Our paper "eVolCheck: Incremental Upgrade Checker for C" has been accepted to TACAS 2013.
Our paper "Using Cross-Entropy for Satisfiability" has been accepted to SAC 2013.
We are co-organizing CAV 2013.
Our paper "Incremental Upgrade Checking by Means of Interpolation-based Function Summaries" has been accepted to FMCAD 2012.
The EU FP7/PINCETTE project got the highest possible score from the annual review performed in Brussels in June. The overall assessment states that the progress in the project has been excellent, and that the project has fully achieved its objectives and technical goals for the period and has even exceeded expectations.
Our paper "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization" has been accepted to ATVA 2012.
Our papers "Leveraging Interpolant Strength in Model Checking" and "SAFARI: SMT-based Abstraction For Arrays with Interpolants" have been accepted to CAV 2012.
Our paper "Interpolation-based Function Summaries in Bounded Model Checking" was accepted to HVC 2011.
Aliaksei Tsitovich received the PhD degree from the University of Lugano, with a thesis titled "Scalable Abstraction for Efficient Security Checks".
Prof. Sharygina and Dr. Bruttomesso are presenting OpenSMT and its applications to verification at MIT SAT/SMT summer school.
Our article on combination of precise and approximated abstractions appeared in International Journal on Software Tools for Technology Transfer (STTT).
Our EU project PINCETTE is in the press SwissInfo.ch: "Tweezers to remove errors".
Alpine Verification Meeting 2010 in Lugano (see photo)
Our EU project PINCETTE is in the press Corriere del Ticino: "Mission: eliminate bugs".
Our paper "An Efficient and Flexible Approach to Resolution Proof Reduction" was accepted to HVC 2010.
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.