News from Formal Verification and Security Group at University of Lugano en FMCAD paper accepted <p>Our paper &quot;<a href="">Incremental Upgrade Checking by Means of Interpolation-based Function Summaries</a>&quot; has been accepted to&nbsp;<a href="">FMCAD 2012</a>.</p> Thu, 21 Jun 2012 11:38:40 +0200 mcWebAdmin 172 at Excellent rating from the EU FP7/PINCETTE annual review <p>The EU FP7/PINCETTE project got the highest possible score from the annual review performed in Brussels in June.&nbsp;The overall assessment states that the progress in the project has been excellent, and that&nbsp;the project has fully achieved its objectives and technical goals for the period and has even exceeded expectations.</p> Fri, 14 Sep 2012 13:53:46 +0200 Antti 175 at ATVA paper accepted <p>Our paper &quot;<a href="">FunFrog: Bounded Model Checking with Interpolation-based Function Summarization</a>&quot; has been accepted to&nbsp;<a href="">ATVA 2012</a>.</p> Wed, 25 Jul 2012 11:22:10 +0200 mcWebAdmin 174 at CAV paper accepted <p>Our papers &quot;<a href="">Leveraging Interpolant Strength in Model&nbsp;Checking</a>&quot; and &quot;<a href="">SAFARI: SMT-based Abstraction For Arrays with Interpolants</a>&quot; have been accepted to <a href="">CAV 2012</a>.</p> Fri, 30 Mar 2012 12:57:12 +0200 Francesco 165 at LPAR 2012 <p>Our paper &quot;<a href="">Lazy Abstraction with Interpolation for Arrays</a>&quot; was accepted to <a href="">LPAR 2012</a>.</p> Wed, 18 Jan 2012 17:22:20 +0100 Francesco 155 at ''Quality of Interpolants in Model Checking'' funded <p>Our project&nbsp;''Quality of Interpolants in Model Checking''<a style="color: rgb(51, 102, 153); " href="">&nbsp;</a>has been funded by&nbsp;<a style="color: rgb(51, 102, 153); " href="">SNSF&nbsp;</a>for 3 years. The correspondent&nbsp;<a href="">position for a PhD</a>&nbsp;student is open now.</p> Thu, 22 Sep 2011 16:22:58 +0200 mcWebAdmin 138 at HVC 2011 <p>Our paper &quot;<a style="color: rgb(51, 102, 153); " href="">Interpolation-based Function Summaries in Bounded Model Checking</a>&quot; was accepted to&nbsp;<a style="color: rgb(51, 102, 153); " href="">HVC 2011</a>.</p> Tue, 20 Sep 2011 15:57:54 +0200 mcWebAdmin 136 at Aliaksei graduated <p>Aliaksei Tsitovich received the PhD degree from the University of Lugano, with a thesis titled &quot;<a href="">Scalable Abstraction for Efficient Security Checks</a>&quot;.<font color="#222222" face="arial, sans-serif" size="2"><span style="line-height: 16px;"><br /> </span></font></p> Wed, 18 Jan 2012 17:36:50 +0100 Francesco 157 at OpenSMT is presented at MIT <p>Prof. Sharygina and Dr. Bruttomesso are presenting OpenSMT and its applications to verification at <a target="_blank" href="">MIT SAT/SMT summer school</a>.</p> Fri, 17 Jun 2011 14:01:54 +0200 Aliaksei 133 at New publication in STTT journal <p>Our <a href="/publications/sharygina-tonetta-tsitovich-2011-abstraction-refinement-approach-combining-precise-and-approximated-techniques">article on combination of precise and approximated abstractions</a> appeared in&nbsp; International Journal on Software Tools for Technology Transfer (STTT).</p> Mon, 02 May 2011 18:15:14 +0200 Aliaksei 132 at A paper on light-weight termination analysis will appear at TACAS'11 <p>Our latest work on the <a href="/loopfrog/termination">summarization-based termination</a> analysis resulted in <a href="/publications/tsitovich-sharygina-wintersteiger-kroening--2011-loop-summarization-and-termination-analysis">the paper</a>, which will be presented at <a href="">TACAS'11</a>.</p> Wed, 12 Jan 2011 04:41:34 +0100 Aliaksei 128 at Our EU project PINCETTE is in the press "Tweezers to remove errors''. <p>Our EU project PINCETTE is in the press <i></i>: <a href="">&quot;Tweezers to remove errors&quot;</a>.</p> Wed, 01 Dec 2010 10:57:38 +0100 Ondrej 123 at AVM 2010 in Lugano <p>Alpine Verification Meeting 2010 in Lugano (see <a href="files/cost-avm-lugano.jpg">photo</a>)</p> Tue, 18 Jan 2011 14:38:30 +0100 Ondrej 129 at Our EU project PINCETTE is in the press Corriere del Ticino: "Mission: eliminate bugs". <p>Our EU project PINCETTE is in the press <i>Corriere del Ticino</i>: <a href="">&quot;Mission: eliminate bugs&quot;</a>.</p> Wed, 01 Dec 2010 11:59:31 +0100 Ondrej 125 at FMCAD 2010 registration is open <p>The&nbsp;<a target="_blank" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; padding-top: 0px; padding-right: 0px; padding-bottom: 0px; padding-left: 0px; text-decoration: none; " href="">registration</a>&nbsp;for&nbsp;<a target="_blank" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; padding-top: 0px; padding-right: 0px; padding-bottom: 0px; padding-left: 0px; text-decoration: none; " href="">FMCAD 2010</a>&nbsp;is open.&nbsp;Our Lab will be pleased to welcome you <p><a href="">read more</a></p> Tue, 07 Sep 2010 14:38:34 +0200 mcWebAdmin 119 at Our paper "An Efficient and Flexible Approach to Resolution Proof Reduction" was accepted to HVC 2010. <p>Our paper &quot;<a href="">An Efficient and Flexible Approach to Resolution Proof Reduction</a>&quot; was accepted to&nbsp;<a href="">HVC 2010</a>.</p> Sat, 09 Oct 2010 16:03:43 +0200 Simone 122 at OpenSMT 1.0 alpha successfully participated in SMTCOMP'10 <p>OpenSMT 1.0 alpha has won 3 categories in <a target="_blank" href="">SMT Competition 2010</a>: QF_IDL, QF_RDL and QF_UFIDL.</p> Mon, 26 Jul 2010 02:44:48 +0200 Aliaksei 115 at A paper accepted to ICCAD 2010 <p>Our paper <a href="/publications/bruttomesso-rollini-sharygina-tsitovich-2010-flexible-interpolation-with-local-proof-transformations">&quot;Flexible Interpolation with Local Proof Transformations&quot;</a>&nbsp;was accepted to <a target="_blank" href="">ICCAD 2010</a>.</p> Tue, 29 Jun 2010 02:44:40 +0200 Aliaksei 114 at Our paper will appear in FACJ 2010 <p>New paper &quot;<a href="/publications/braghin-sharygina-barone-adesi-2010-model-checking-based-approach-security-policy-veri%EF%AC%81cation">A Model Checking-based Approach for Security Policy Veriļ¬cation of Mobile Systems</a>&quot; will appear in the&nbsp;<a target="_blank" href="">Formal Aspects of Computing Journal</a>.</p> Wed, 12 May 2010 18:21:12 +0200 Aliaksei 111 at A paper accepted to Memocode 2010 <p>&quot;<a href="/publications/bruttomesso-pek-sharygina-2010-flexible-schema-generating-explanations-lazy-theory-propagation">A Flexible Schema for Generating Explanations in Lazy Theory Propagation</a>&quot; paper was accepted to <a target="_blank" href="">Memocode 2010</a>.</p> Wed, 12 May 2010 15:12:26 +0200 Aliaksei 108 at