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