[llvm-commits] CVS: llvm-www/ProjectsWithLLVM/index.html

[Chris Lattner]

Changes in directory llvm-www/ProjectsWithLLVM:

index.html updated: 1.34 -> 1.35
---
Log message:

add the calysto checker


---
Diffs of the changes:  (+56 -0)

 index.html |   56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 files changed, 56 insertions(+)


Index: llvm-www/ProjectsWithLLVM/index.html
diff -u llvm-www/ProjectsWithLLVM/index.html:1.34 llvm-www/ProjectsWithLLVM/index.html:1.35
--- llvm-www/ProjectsWithLLVM/index.html:1.34	Mon Mar 26 14:05:37 2007
+++ llvm-www/ProjectsWithLLVM/index.html	Mon Apr 23 10:39:59 2007
@@ -35,6 +35,7 @@
 <div class="www_text">
 
 <ul>
+<li><a href="#Calysto">Calysto Static Checker</a></li>
 <li><a href="#ssa_ra">Improvements on SSA-Based Register Allocation</a></li>
 <li><a href="#LENS">LENS Project</a></li>
 <li><a href="#trident">Trident Compiler</a></li>
@@ -57,6 +58,61 @@
 
 <!--=========================================================================-->
 <div class="www_subsection">
+<a name="Calysto">Calysto Static Checker</a>
+<br>
+</div>
+<!--=========================================================================-->
+
+<div class="www_subsubsection">
+By Domagoj Babic, UBC.
+</div>
+
+<div class="www_text">
+
+<p>
+<a href="http://www.cs.ubc.ca/~babic/index_calysto.htm">Calysto</a>
+is a scalable context- and path-sensitive SSA-based static
+assertion checker. Unlike other static
+checkers, Calysto analyzes SSA directly, which means that it not only
+checks the original code, but also the front-end (including
+SSA-optimizations) of the compiler which
+was used to compile the code. The advantage of doing static checking on
+the SSA is language independency and the fact that the checked code is much
+closer to the generated assembly than the source code.
+</p>
+
+<p>
+Several main factors contribute to Calysto's scalability:
+   <ul>
+     <li> A novel SSA symbolic execution algorithm that exploits the
+     structure of the control flow graph to minimize the number of
+     paths that need to be considered.</li>
+
+     <li> Lazy interprocedural analysis.</li>
+     <li> Tight integration with the
+       <a href="http://www.cs.ubc.ca/~babic/index_spear.htm">Spear</a>
+       automated theorem prover, designed for software static
+       checking.</li>
+     <li> And, of course, fast implementations of the basic algorithms
+     in LLVM (dominator trees, postdominance, etc.).</li>
+  </ul>
+</p>
+
+<p>
+Currently, Calysto is still in the development phase, and the first results
+are encouraging. Most likely, the first public release will happen some
+time in the fall 2007.
+<a href="http://www.cs.ubc.ca/~babic/index_spear.htm">Spear</a>
+and Calysto generated
+<a href="http://www.cs.ubc.ca/~babic/index_benchmarks.htm">benchmarks</a>
+are available.
+</p>
+
+</div>
+
+
+<!--=========================================================================-->
+<div class="www_subsection">
   <a name="ssa_ra">Improvements on SSA-Based Register Allocation.</a>
 </div>