[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