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> _______________________________________________ llvm-commits mailing list llvm-commits@cs.uiuc.edu http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits