Uncategorized http://verify.inf.unisi.ch/tools/ Lists all the tools en OpenSMT http://verify.inf.unisi.ch/opensmt <p>As a part of <a href="/projects/smt">research on decision procedures</a>, our Lab develops a tool, OpenSMT, that is used as a framework to perform all our experiments.</p> <p><img hspace="2" height="60" width="200" vspace="2" align="right" alt="OpenSMT" src="http://www.inf.unisi.ch/postdoc/bruttomesso/imgs/small_header.gif" /></p> <p>OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine of formal verification. OpenSMT is built on top of MiniSAT (<a href="http://minisat.se" title="http://minisat.se">http://minisat.se</a>).</p> <p><a href="http://verify.inf.unisi.ch/opensmt">read more</a></p> Tue, 16 Sep 2008 16:02:46 +0200 Roberto 62 at http://verify.inf.unisi.ch Loopfrog http://verify.inf.unisi.ch/loopfrog <p>As a part of the &quot;<a href="/projects/DSFVGMC">Detection of Security Flaws and Vulnerabilities by Guided Model Checking</a>&quot; project we implemented the tool called Loopfrog - an Abstract Interpretation based static analyzer for C programs.</p> <p><a href="http://verify.inf.unisi.ch/loopfrog">read more</a></p> Mon, 03 Dec 2007 17:44:03 +0100 mcWebAdmin 36 at http://verify.inf.unisi.ch eVolCheck http://verify.inf.unisi.ch/evolcheck <p>eVolCheck is a bounded upgrade checker of C, built on the top of <a href="http://www.verify.inf.unisi.ch/funfrog">FunFrog</a>.&nbsp;It uses interpolation-based function summaries, extracted from original version of a program, for incremental verification of an upgraded version of the program.</p> <p>In each incremental check, eVolCheck first identifies the modified function on the syntactical&nbsp;level and then attempts to show that the old function summaries are still valid over-approximations of the behaviour of the modified functions. These are local and thus cheap&nbsp;checks.</p> <p><a href="http://verify.inf.unisi.ch/evolcheck">read more</a></p> Tue, 05 Jun 2012 22:00:22 +0200 mcWebAdmin 166 at http://verify.inf.unisi.ch SAFARI http://verify.inf.unisi.ch/safari <p>SAFARI - SMT-based Abstraction For Arrays with Interpolants - is a model checker designed to prove safety (possibly universally quantified) properties of imperative programs with arrays. SAFARI is based on an extension of the Lazy Abstraction paradigm capable of handling existentially quantified formulae by using a combination of quantifier-free interpolation algorithms for the indexes and elements in the arrays during refinement. <p><a href="http://verify.inf.unisi.ch/safari">read more</a></p> Wed, 18 Jan 2012 14:47:55 +0100 Francesco 148 at http://verify.inf.unisi.ch FunFrog http://verify.inf.unisi.ch/funfrog <p>FunFrog is a bounded model checker of C using interpolation-based function summaries. FunFrog uses Craig interpolation to extract function summaries and reuses them in subsequent verification runs as a means of over-approximation of the precise functions' behavior.</p> <p>To deal with spurious errors, which are possible due to the over-approximation, FunFrog employs a counter-example guided refinement strategy to identify too coarse summaries responsible for the error trace and replaces those with precise behavior representation in the next iteration.</p> <p><a href="http://verify.inf.unisi.ch/funfrog">read more</a></p> Tue, 16 Aug 2011 15:08:43 +0200 Ondrej 134 at http://verify.inf.unisi.ch Synergy http://verify.inf.unisi.ch/projects/synergy/tool <p>The techniques developed for &nbsp;&quot;<a href="/projects/synergy">The Synergy of Precise and Fast Abstractions for Program Verification</a>&quot; project are implemented on top of SATABS model-checker for ANSI-C programs. The tool allows to compare effectiveness of abstraction techniques in CEGAR-based verification. Details of the techniques can be found in <span hovertip="reference1">[1]</span>.</p> <p><a href="/files/tool.tar.bz">Tool binary </a>(1,6MB) compiled for Linux/i386.</p> <p><hr /><p><h3>References</h3></p><div class="references"><ol><li id="reference1"><span class="biblio-title"><a href="/publications/sharygina-tonetta-tsitovich-2009-synergy">The Synergy of Precise and Fast Abstractions for Program Verification</a></span>, <span class="biblio-authors">Sharygina, N.; Tonetta, S.; Tsitovich, A.</span> , 24th Annual ACM Symposium on Applied Computing (SAC), Honolulu, USA, p.566-573, ACM (2009) <span class="Z3988" title="ctx_ver=Z39.88-2004&amp;rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&amp;rfr_id=info%3Asid%2Fwww.verify.inf.usi.ch&amp;rft.title=The+Synergy+of+Precise+and+Fast+Abstractions+for+Program+Veri%EF%AC%81cation&amp;rft.date=2009&amp;rft.spage=566&amp;rft.epage=573&amp;rft.aulast=Sharygina&amp;rft.aufirst=Natasha&amp;rft.au=Tonetta%2C+Stefano&amp;rft.au=Tsitovich%2C+Aliaksei&amp;rft.pub=ACM&amp;rft.place=Honolulu%2C+USA&amp;rft_id=http%3A%2F%2Fdx.doi.org%2F10.1145%2F1529282.1529404"></span> </li> </ol></div> Sat, 25 Oct 2008 22:38:13 +0200 mcWebAdmin 70 at http://verify.inf.unisi.ch Boppo http://verify.inf.unisi.ch/boppo <p>Boppo is a model checker for Boolean programs. Features:</p> <ul> <li>Partial Order Reduction</li> <li>Fixpoint detection using QBF</li> <li>Support for the constrain construct</li> </ul> <p>&nbsp;<br /> It is a joint product of Byron Cook, Daniel Kroening, and Natasha Sharygina.<br /> <a href="http://www.cprover.org/boppo/">Download Boppo</a></p> Wed, 13 Feb 2008 12:23:03 +0100 Aliaksei 44 at http://verify.inf.unisi.ch SATABS http://verify.inf.unisi.ch/satabs <p>SATABS is a verification tool for ANSI-C and C++ programs. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check ANSI-C and C++ for consistency with other languages, such as Verilog. SATABS computes an abstraction of the program in order to handle large amounts of code. <a href="http://www.cprover.org/satabs/">SATABS home page</a><br /> &nbsp;</p> Wed, 13 Feb 2008 11:47:35 +0100 Aliaksei 43 at http://verify.inf.unisi.ch