[llvm-commits] CVS: llvm-www/pubs/2008-09-ASE-FrameAxioms.html 2008-09-ASE-FrameAxioms.pdf pubs.js

Tue Mar 24 22:52:28 PDT 2009

Changes in directory llvm-www/pubs:

2008-09-ASE-FrameAxioms.html added (r1.1)
2008-09-ASE-FrameAxioms.pdf added (r1.1)
pubs.js updated: 1.10 -> 1.11
---
Log message:

add a paper.


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

 2008-09-ASE-FrameAxioms.html |   47 +++++++++++++++++++++++++++++++++++++++++++
 2008-09-ASE-FrameAxioms.pdf  |    0 
 pubs.js                      |    8 +++++++
 3 files changed, 55 insertions(+)


Index: llvm-www/pubs/2008-09-ASE-FrameAxioms.html
diff -c /dev/null llvm-www/pubs/2008-09-ASE-FrameAxioms.html:1.1
*** /dev/null	Wed Mar 25 00:49:41 2009

--- llvm-www/pubs/2008-09-ASE-FrameAxioms.html	Wed Mar 25 00:49:31 2009
***************
*** 0 ****
--- 1,47 ----
+ <!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="http://llvm.org/llvm.css" type="text/css" media="screen" />
+   <title>Automatic Inference of Frame Axioms Using Static Analysis</title>
+ </head>
+ <body>
+ 
+ <div class="pub_title">
+   Automatic Inference of Frame Axioms Using Static Analysis
+ </div>
+ <div class="pub_author">
+   Zvonimir Rakamaric and Alan J. Hu
+ </div>
+ 
+ <h2>Abstract:</h2>
+ <blockquote>
+ 
+ Many approaches to software verification are currently 
+ semi-automatic: a human must provide key logical insights 
+ — e.g., loop invariants, class invariants, and frame axioms 
+ that limit the scope of changes that must be analyzed. 
+ This paper describes a technique for automatically inferring frame 
+ axioms of procedures and loops using static 
+ analysis. The technique builds on a pointer analysis 
+ that generates limited information about all data structures 
+ in the heap. Our technique uses that information 
+ to over-approximate a potentially unbounded set of memory 
+ locations modified by each procedure/loop; this over-approximation 
+ is a candidate frame axiom. 
+ We have tested this approach on the buffer-overﬂow 
+ benchmarks from ASE 2007. With manually provided specifications 
+ and invariants/axioms, our tool could verify/falsify 
+ 226 of the 289 benchmarks. With our automatically inferred 
+ frame axioms, the tool could verify/falsify 203 of the 289, 
+ demonstrating the effectiveness of our approach. 
+ 
+ </blockquote>
+ 
+ <h2>Download:</h2>
+ <ul>
+   <li><a href="2008-09-ASE-FrameAxioms.pdf">Automatic Inference of Frame Axioms Using Static Analysis</a> (PDF)</li>
+ </ul>
+ 
+ </body>
+ </html>


Index: llvm-www/pubs/2008-09-ASE-FrameAxioms.pdf


Index: llvm-www/pubs/pubs.js
diff -u llvm-www/pubs/pubs.js:1.10 llvm-www/pubs/pubs.js:1.11
--- llvm-www/pubs/pubs.js:1.10	Tue Mar 24 19:22:00 2009
+++ llvm-www/pubs/pubs.js	Wed Mar 25 00:49:31 2009
@@ -52,6 +52,14 @@
    month: 10,
    year: 2008},
 
+  {url: '2008-09-ASE-FrameAxioms.html',
+   title: 'Automatic Inference of Frame Axioms Using Static Analysis',
+   author: 'Zvonimir Rakamaric and Alan J. Hu',
+   published: '23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008)',
+   month: 9,
+   year: 2008,
+   location: "L'Aquila, Italy"},
+
   {url: '2008-09-LadyVM.html',
    title: 'A Lazy Developer Approach: Building a JVM with Third Party Software',
    author: 'Nicolas Geoffray, Gael Thomas, Charles Clement and Bertil Folliot',




