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.htmlThu 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
+ titleStructural 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
+
+ h2Abstract:/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
+
+ h2Published:/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
+
+ h2Download:/h2
+ h3Paper:/h3
+ ul
+ li
+ a href=2007-07-CAV-StructuralAbstraction.pdf
+ Structural Abstraction of Software Verification Conditions
+ /a (PDF)
+ /li
+ /ul
+
+ h2BibTeX 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.htmlThu Apr 26 23:57:07 2007
@@ -3,6 +3,12 @@
ol
+lia href=2007-07-CAV-StructuralAbstraction.htmlStructural Abstraction of
+ Software Verification Conditions/abr
+ Domagoj Babic and Alan J. Hu.br
+ iProc. of the 19th Int. Conf. on Computer Aided Verification
+ (CAV'07)/i, Berlin, Germany, Jul, 2007.br/li
+
lia href=2007-06-10-PLDI-DSA.htmlMaking Context-Sensitive Points-to
Analysis with Heap Cloning Practical For The Real World/abr
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
