[www] r235600 - Added SMACK to the LLVM Projects page.
John Criswell
criswell at uiuc.edu
Thu Apr 23 07:35:54 PDT 2015
Author: criswell
Date: Thu Apr 23 09:35:54 2015
New Revision: 235600
URL: http://llvm.org/viewvc/llvm-project?rev=235600&view=rev
Log:
Added SMACK to the LLVM Projects page.
Added SMACK to the list of LLVM Users.
Modified:
www/trunk/ProjectsWithLLVM/index.html
www/trunk/Users.html
Modified: www/trunk/ProjectsWithLLVM/index.html
URL: http://llvm.org/viewvc/llvm-project/www/trunk/ProjectsWithLLVM/index.html?rev=235600&r1=235599&r2=235600&view=diff
==============================================================================
--- www/trunk/ProjectsWithLLVM/index.html (original)
+++ www/trunk/ProjectsWithLLVM/index.html Thu Apr 23 09:35:54 2015
@@ -36,6 +36,7 @@
<div class="www_text">
<ul>
+<li><a href="#smack">SMACK Software Verifier</a></li>
<li><a href="#discopop">DiscoPoP: A Parallelism Discovery Tool</a></li>
<li><a href="#jade">Just-in-time Adaptive Decoder Engine (Jade)</a></li>
<li><a href="#crack">The Crack Programming Language</a></li>
@@ -75,6 +76,27 @@
</div>
<!--=========================================================================-->
+<div class="www_subsection">
+<a name="smack">SMACK Software Verifier</a>
+</div>
+
+<div class="www_subsubsection">
+ By <a href="https://github.com/smackers/smack/wiki/Smackers">smackers</a>
+</div>
+
+<div class="www_text">
+ <p>
+ <a href="https://github.com/smackers/smack">SMACK</a> is an automated
+ software verifier, verifying assertions given in its input LLVM
+ intermediate representation (IR) programs. Under the hood, SMACK is a
+ translator from the LLVM IR into the Boogie intermediate verification
+ language (IVL). Targeting Boogie exploits a canonical platform which
+ simplifies the implementation of algorithms for verification, model
+ checking, and abstract interpretation.
+ </p>
+</div>
+
+<!--=========================================================================-->
<div class="www_subsection">
<a name="discopop">DiscoPoP: A Parallelism Discovery Tool</a>
</div>
Modified: www/trunk/Users.html
URL: http://llvm.org/viewvc/llvm-project/www/trunk/Users.html?rev=235600&r1=235599&r2=235600&view=diff
==============================================================================
--- www/trunk/Users.html (original)
+++ www/trunk/Users.html Thu Apr 23 09:35:54 2015
@@ -295,6 +295,11 @@ multi-core code generation to the compil
</tr>
<tr>
+ <td><a href="https://github.com/smackers/smack">SMACK Software Verifier</a></td>
+ <td>Software verifier that converts LLVM IR to Boogie</td>
+ </tr>
+
+ <tr>
<td><a href="http://objective.modula2.net">Objective Modula-2 Project</a></td>
<td>Modula-2 compiler w/ObjC runtime support. Targets Objective-C and LLVM.</td>
</tr>
More information about the llvm-commits
mailing list