[llvm-commits] CVS: llvm-www/pubs/2007-07-CAV-StructuralAbstraction.html 2007-07-CAV-StructuralAbstraction.pdf index.html

Thu Apr 26 21:57:25 PDT 2007

Changes in directory llvm-www/pubs:

2007-07-CAV-StructuralAbstraction.html added (r1.1)
2007-07-CAV-StructuralAbstraction.pdf added (r1.1)
index.html updated: 1.47 -> 1.48
---
Log message:

Add Domagoj's paper


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

 2007-07-CAV-StructuralAbstraction.html |   81 +++++++++++++++++++++++++++++++++
 2007-07-CAV-StructuralAbstraction.pdf  |    0 
 index.html                             |    6 ++
 3 files changed, 87 insertions(+)


Index: llvm-www/pubs/2007-07-CAV-StructuralAbstraction.html
diff -c /dev/null llvm-www/pubs/2007-07-CAV-StructuralAbstraction.html:1.1
*** /dev/null	Thu Apr 26 23:57:17 2007

--- llvm-www/pubs/2007-07-CAV-StructuralAbstraction.html	Thu Apr 26 23:57:07 2007
***************
*** 0 ****
--- 1,81 ----
+ <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+ <html>
+ <head>
+   <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
+   <link rel="stylesheet" href="../llvm.css" type="text/css" media="screen">
+   <title>Structural Abstraction of Software Verification Conditions</title>
+ </head>
+ 
+ <body>
+ 
+ <div class="pub_title">
+ Structural Abstraction of Software Verification Conditions
+ </div>
+ 
+ <div class="pub_author">
+   <a href="http://www.cs.ubc.ca/~babic">Domagoj Babic</a>
+   and
+   <a href="http://www.cs.ubc.ca/~ajh">Alan J. Hu</a>
+ </div>
+ 
+ <h2>Abstract:</h2>
+ <blockquote>
+ Precise software analysis and verification require tracking the exact
+ path along which a statement is executed (path-sensitivity), the different contexts
+ from which a function is called (context-sensitivity), and the bit-accurate
+ operations performed. Previously, verification with such precision has been considered
+ too inefficient to scale to large software. In this paper, we present
+ a novel approach to solving such verification conditions, based on an automatic
+ abstraction-checking-refinement framework that exploits natural abstraction
+ boundaries present in software. Experimental results show that our approach
+ easily scales to over 200,000 lines of real C/C++ code.
+ </blockquote>
+ 
+ <h2>Published:</h2>
+ 
+ <blockquote>
+ "Structural Abstraction of Software Verification Conditions"
+ <br>
+ Domagoj Babic and Alan J. Hu.
+ <br>
+ <i>
+     Proc. of the 19th International Conference on
+     Computer Aided Verification (CAV'07)
+ </i>,
+ Berlin, Germany, July 3-7, 2007.
+ </blockquote>
+ 
+ <h2>Download:</h2>
+ <h3>Paper:</h3>
+ <ul>
+ <li>
+ "<a href="2007-07-CAV-StructuralAbstraction.pdf">
+ Structural Abstraction of Software Verification Conditions
+ </a>" (PDF)
+ </li>
+ </ul>
+ 
+ <h2>BibTeX Entry:</h2>
+ <pre>
+ @inproceedings{bh07structural,
+   author = {Domagoj Babi\'c and Alan J. Hu},
+   title = {{Structural Abstraction of Software Verification Conditions}},
+   booktitle = {Proceedings of the 19th Int. Conf. on Computer Aided Verification
+                (CAV'07), Berlin, Germany}
+   publisher = {Springer},
+   series = {Lecture Notes in Computer Science},
+   year = {2007},
+   month = {July}
+ }
+ </pre>
+ 
+ <!-- *********************************************************************** -->
+ <hr>
+   <a href="http://jigsaw.w3.org/css-validator/check/referer"><img
+   src="http://jigsaw.w3.org/css-validator/images/vcss" alt="Valid CSS!"></a>
+ 
+   <a href="http://validator.w3.org/check/referer"><img
+   src="http://www.w3.org/Icons/valid-html401" alt="Valid HTML 4.01!" /></a>
+ 
+ </body>
+ </html>


Index: llvm-www/pubs/2007-07-CAV-StructuralAbstraction.pdf


Index: llvm-www/pubs/index.html
diff -u llvm-www/pubs/index.html:1.47 llvm-www/pubs/index.html:1.48
--- llvm-www/pubs/index.html:1.47	Sun Apr  8 23:06:31 2007
+++ llvm-www/pubs/index.html	Thu Apr 26 23:57:07 2007
@@ -3,6 +3,12 @@
 
 <ol>
 
+<li>"<a href="2007-07-CAV-StructuralAbstraction.html">Structural Abstraction of
+  Software Verification Conditions</a>"<br>
+  Domagoj Babic and Alan J. Hu.<br>
+  <i>Proc. of the 19th Int. Conf. on Computer Aided Verification
+               (CAV'07)</i>, Berlin, Germany, Jul, 2007.<br></li>
+
 <li>"<a href="2007-06-10-PLDI-DSA.html">Making Context-Sensitive Points-to
     Analysis with Heap Cloning Practical For The Real World</a>"<br>
   Chris Lattner, Andrew Lenharth, and Vikram Adve.<br>




