News from Formal Verification and Security Group at University of Lugano

FMCAD paper accepted

mcWebAdmin — Thu, 21 Jun 2012 11:38:40 +0200

Our paper "Incremental Upgrade Checking by Means of Interpolation-based Function Summaries" has been accepted to FMCAD 2012.

Excellent rating from the EU FP7/PINCETTE annual review

Antti — Fri, 14 Sep 2012 13:53:46 +0200

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.

ATVA paper accepted

mcWebAdmin — Wed, 25 Jul 2012 11:22:10 +0200

Our paper "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization" has been accepted to ATVA 2012.

CAV paper accepted

Francesco — Fri, 30 Mar 2012 12:57:12 +0200

Our papers "Leveraging Interpolant Strength in Model Checking" and "SAFARI: SMT-based Abstraction For Arrays with Interpolants" have been accepted to CAV 2012.

LPAR 2012

Francesco — Wed, 18 Jan 2012 17:22:20 +0100

Our paper "Lazy Abstraction with Interpolation for Arrays" was accepted to LPAR 2012.

''Quality of Interpolants in Model Checking'' funded

mcWebAdmin — Thu, 22 Sep 2011 16:22:58 +0200

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.

HVC 2011

mcWebAdmin — Tue, 20 Sep 2011 15:57:54 +0200

Our paper "Interpolation-based Function Summaries in Bounded Model Checking" was accepted to HVC 2011.

Aliaksei graduated

Francesco — Wed, 18 Jan 2012 17:36:50 +0100

Aliaksei Tsitovich received the PhD degree from the University of Lugano, with a thesis titled "Scalable Abstraction for Efficient Security Checks".

OpenSMT is presented at MIT

Aliaksei — Fri, 17 Jun 2011 14:01:54 +0200

Prof. Sharygina and Dr. Bruttomesso are presenting OpenSMT and its applications to verification at MIT SAT/SMT summer school.

New publication in STTT journal

Aliaksei — Mon, 02 May 2011 18:15:14 +0200

Our article on combination of precise and approximated abstractions appeared in International Journal on Software Tools for Technology Transfer (STTT).

A paper on light-weight termination analysis will appear at TACAS'11

Aliaksei — Wed, 12 Jan 2011 04:41:34 +0100

Our latest work on the summarization-based termination analysis resulted in the paper, which will be presented at TACAS'11.

Our EU project PINCETTE is in the press SwissInfo.ch: "Tweezers to remove errors''.

Ondrej — Wed, 01 Dec 2010 10:57:38 +0100

Our EU project PINCETTE is in the press SwissInfo.ch: "Tweezers to remove errors".

AVM 2010 in Lugano

Ondrej — Tue, 18 Jan 2011 14:38:30 +0100

Alpine Verification Meeting 2010 in Lugano (see photo)

Our EU project PINCETTE is in the press Corriere del Ticino: "Mission: eliminate bugs".

Ondrej — Wed, 01 Dec 2010 11:59:31 +0100

Our EU project PINCETTE is in the press Corriere del Ticino: "Mission: eliminate bugs".

FMCAD 2010 registration is open

mcWebAdmin — Tue, 07 Sep 2010 14:38:34 +0200

The registration for FMCAD 2010 is open. Our Lab will be pleased to welcome you

Our paper "An Efficient and Flexible Approach to Resolution Proof Reduction" was accepted to HVC 2010.

Simone — Sat, 09 Oct 2010 16:03:43 +0200

Our paper "An Efficient and Flexible Approach to Resolution Proof Reduction" was accepted to HVC 2010.

OpenSMT 1.0 alpha successfully participated in SMTCOMP'10

Aliaksei — Mon, 26 Jul 2010 02:44:48 +0200

OpenSMT 1.0 alpha has won 3 categories in SMT Competition 2010: QF_IDL, QF_RDL and QF_UFIDL.

A paper accepted to ICCAD 2010

Aliaksei — Tue, 29 Jun 2010 02:44:40 +0200

Our paper "Flexible Interpolation with Local Proof Transformations" was accepted to ICCAD 2010.

Our paper will appear in FACJ 2010

Aliaksei — Wed, 12 May 2010 18:21:12 +0200

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 paper accepted to Memocode 2010

Aliaksei — Wed, 12 May 2010 15:12:26 +0200

"A Flexible Schema for Generating Explanations in Lazy Theory Propagation" paper was accepted to Memocode 2010.