[llvm-commits] [www-pubs] r118779 - in /www-pubs/trunk: 2010-07-CAV-LazyAnnot.html 2010-07-CAV-LazyAnnot.pdf pubs.js

Wed Nov 10 23:16:18 PST 2010

Author: lattner
Date: Thu Nov 11 01:16:18 2010
New Revision: 118779

URL: http://llvm.org/viewvc/llvm-project?rev=118779&view=rev
Log:
add a paper nuno pointed me at

Added:
    www-pubs/trunk/2010-07-CAV-LazyAnnot.html
    www-pubs/trunk/2010-07-CAV-LazyAnnot.pdf   (with props)
Modified:
    www-pubs/trunk/pubs.js

Added: www-pubs/trunk/2010-07-CAV-LazyAnnot.html
URL: http://llvm.org/viewvc/llvm-project/www-pubs/trunk/2010-07-CAV-LazyAnnot.html?rev=118779&view=auto
==============================================================================

--- www-pubs/trunk/2010-07-CAV-LazyAnnot.html (added)
+++ www-pubs/trunk/2010-07-CAV-LazyAnnot.html Thu Nov 11 01:16:18 2010
@@ -0,0 +1,69 @@
+<!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>Lazy Annotation for Program Testing and Verification</title>
+</head>
+<body>
+
+<div class="pub_title">
+  Lazy Annotation for Program Testing and Verification
+</div>
+<div class="pub_author">
+  Kenneth McMillan
+</div>
+
+<h2>Abstract:</h2>
+<blockquote>
+<p>
+We describe an interpolant-based approach to test generation and model checking for sequential programs. The method generates Floyd/Hoare style annotations of the program on demand, as a result of failure to achieve goals, in a manner analogous to conflict clause learning in a DPLL style SAT solver.
+</p>
+</blockquote>
+
+<h2>Published:</h2>
+<blockquote>
+  "Lazy Annotation for Program Testing and Verification"<br>
+   Kenneth McMillan<br>
+<i>In Proceedings of Computer Aided Verification,</i>
+Edinburgh, UK, July 15-19, 2010.
+</blockquote>
+
+<h2>Download:</h2>
+<h3>Paper:</h3>
+<ul>
+  <li><a href="2010-07-CAV-LazyAnnot.pdf">
+  Lazy Annotation for Program Testing and Verification
+  </a> (PDF)</li>
+</ul>
+
+<h2>BibTeX Entry:</h2>
+<pre>
+ at incollection {springerlink:10.1007/978-3-642-14295-6_10,
+   author = {McMillan, Kenneth},
+   affiliation = {Cadence Berkeley Labs},
+   title = {Lazy Annotation for Program Testing and Verification},
+   booktitle = {Computer Aided Verification},
+   series = {Lecture Notes in Computer Science},
+   editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul},
+   publisher = {Springer Berlin / Heidelberg},
+   isbn = {},
+   pages = {104-118},
+   volume = {6174},
+   url = {http://dx.doi.org/10.1007/978-3-642-14295-6_10},
+   note = {10.1007/978-3-642-14295-6_10},
+   abstract = {We describe an interpolant-based approach to test generation and model checking for sequential programs. The method generates Floyd/Hoare style annotations of the program on demand, as a result of failure to achieve goals, in a manner analogous to conflict clause learning in a DPLL style SAT solver.},
+   year = {2010}
+}
+</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>

Added: www-pubs/trunk/2010-07-CAV-LazyAnnot.pdf
URL: http://llvm.org/viewvc/llvm-project/www-pubs/trunk/2010-07-CAV-LazyAnnot.pdf?rev=118779&view=auto
==============================================================================
Binary file - no diff available.

Propchange: www-pubs/trunk/2010-07-CAV-LazyAnnot.pdf
------------------------------------------------------------------------------
    svn:mime-type = application/octet-stream

Modified: www-pubs/trunk/pubs.js
URL: http://llvm.org/viewvc/llvm-project/www-pubs/trunk/pubs.js?rev=118779&r1=118778&r2=118779&view=diff
==============================================================================
--- www-pubs/trunk/pubs.js (original)
+++ www-pubs/trunk/pubs.js Thu Nov 11 01:16:18 2010
@@ -15,6 +15,18 @@
    author: "André Tavares, Fernando Magno Pereira, Mariza Bigonha and Roberto Bigonha",
    month: 9,
    year: 2010},
+
+  {
+            url: "2010-07-CAV-LazyAnnot.html",
+            title: "Lazy Annotation for Program Testing and Verification",
+            published: "In Proceedings of Computer Aided Verification (CAV 2010)",
+            author: "Kenneth McMillan",
+            location: "Edinburgh, UK",
+            month: 7,
+            year: 2010
+  },
+            
+            
   {url: "2010-06-ISCA-Relax.html",
    title: "Relax: An Architectural Framework for Software Recovery of Hardware Faults",
    published: "ISCA '10: International Symposium on Computer Architecture",



