[llvm-commits] CVS: llvm-www/pubs/2008-11-PASTE-CompilerValidation.html 2008-11-PASTE-CompilerValidation.pdf pubs.js

Sat Jun 27 12:11:05 PDT 2009

Changes in directory llvm-www/pubs:

2008-11-PASTE-CompilerValidation.html added (r1.1)
2008-11-PASTE-CompilerValidation.pdf added (r1.1)
pubs.js updated: 1.28 -> 1.29
---
Log message:

add "Program analysis for compiler validation" from PASTE'08


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

 2008-11-PASTE-CompilerValidation.html |   64 ++++++++++++++++++++++++++++++++++
 2008-11-PASTE-CompilerValidation.pdf  |    0 
 pubs.js                               |    8 ++++
 3 files changed, 72 insertions(+)


Index: llvm-www/pubs/2008-11-PASTE-CompilerValidation.html
diff -c /dev/null llvm-www/pubs/2008-11-PASTE-CompilerValidation.html:1.1
*** /dev/null	Sat Jun 27 14:10:55 2009

--- llvm-www/pubs/2008-11-PASTE-CompilerValidation.html	Sat Jun 27 14:10:45 2009
***************
*** 0 ****
--- 1,64 ----
+ <!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>Program Analysis for Compiler Validation</title>
+ </head>
+ <body>
+ 
+ <div class="pub_title">
+   Program Analysis for Compiler Validation
+ </div>
+ <div class="pub_author">
+   Anna Zaks and Amir Pnueli
+ </div>
+ 
+ <h2>Abstract:</h2>
+ <blockquote>
+ Translation Validation is an approach of ensuring compilation correctness in which each compiler run is followed by a validation pass that proves that the target code produced by the compiler is a correct translation (implementation) of the source code. It has been previously shown that the problem of translation validation can be reduced to checking if a single system - the corss-product of the source and target, satisfies a specific property. In this paper, we show how to adapt the existing program analysis techniques in the setting of translation validation. In addition, we present a novel invariant generation algorithm which strengthens our analysis when the input programs contain dynamically allocated data structures. Finally, we report on the prototype tool that applies the developed methodology to verification of the LLVM compiler. The tool handles many of the classical intraprocedural compiler optimizations such as constant folding, reassociation, common subexpress!
 ion elimination, code motion, dead code elimination, and others.
+ </blockquote>
+ 
+ <h2>Published:</h2>
+ <blockquote>
+   "Program Analysis for Compiler Validation"
+   <br>
+   Anna Zaks and Amir Pnueli.
+   <br>
+ <i>
+ Workshop on Program Analysis for Software Tools and Engineering (PASTE'08)
+ </i>, Atlanta, GA, November 2008.
+ </blockquote>
+ <h2>Download:</h2>
+ <h3>Paper:</h3>
+ <ul>
+   <li><a href="2008-11-PASTE-CompilerValidation.pdf">
+   Program Analysis for Compiler Validation
+   </a> (PDF)</li>
+ </ul>
+ 
+ <h2>BibTeX Entry:</h2>
+ <pre>
+ @inproceedings{1512477,
+  author = {Zaks, Anna and Pnueli, Amir},
+  title = {Program analysis for compiler validation},
+  booktitle = {PASTE '08: Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering},
+  year = {2008},
+  isbn = {978-1-60558-382-2},
+  pages = {1--7},
+  location = {Atlanta, Georgia},
+  doi = {http://doi.acm.org/10.1145/1512475.1512477},
+  publisher = {ACM},
+  address = {New York, NY, USA},
+  }
+ </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/2008-11-PASTE-CompilerValidation.pdf


Index: llvm-www/pubs/pubs.js
diff -u llvm-www/pubs/pubs.js:1.28 llvm-www/pubs/pubs.js:1.29
--- llvm-www/pubs/pubs.js:1.28	Sat Jun 27 14:03:32 2009
+++ llvm-www/pubs/pubs.js	Sat Jun 27 14:10:45 2009
@@ -164,6 +164,14 @@
    month: 11,
    year: 2008},
 
+  {url: '2008-11-PASTE-CompilerValidation.html',
+   title: "Program analysis for compiler validation",
+   author: "Anna Zaks and Amir Pnueli",
+   published: "Proc. of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering (PASTE'08)",
+   location: "Atlanta, Georgia",
+   month: 11,
+   year: 2008},
+
   {url: '2008-10-04-ACAT-LLVM-Intro.html',
    title: 'Introduction to the LLVM Compiler System',
    author: 'Chris Lattner',




