[llvm-commits] CVS: llvm-www/pubs/2009-06-HotDep-SymbolicExec.html 2009-06-HotDep-SymbolicExec.pdf pubs.js

Chris Lattner sabre at nondot.org
Sun Sep 20 10:03:21 PDT 2009



Changes in directory llvm-www/pubs:

2009-06-HotDep-SymbolicExec.html added (r1.1)
2009-06-HotDep-SymbolicExec.pdf added (r1.1)
pubs.js updated: 1.49 -> 1.50
---
Log message:

add a new paper.


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

 2009-06-HotDep-SymbolicExec.html |   48 +++++++++++++++++++++++++++++++++++++++
 2009-06-HotDep-SymbolicExec.pdf  |    0 
 pubs.js                          |    8 ++++++
 3 files changed, 56 insertions(+)


Index: llvm-www/pubs/2009-06-HotDep-SymbolicExec.html
diff -c /dev/null llvm-www/pubs/2009-06-HotDep-SymbolicExec.html:1.1
*** /dev/null	Sun Sep 20 12:02:26 2009
--- llvm-www/pubs/2009-06-HotDep-SymbolicExec.html	Sun Sep 20 12:02:16 2009
***************
*** 0 ****
--- 1,48 ----
+ <!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>Selective Symbolic Execution</title>
+ </head>
+ <body>
+ 
+ <div class="pub_title">
+   Selective Symbolic Execution
+ </div>
+ <div class="pub_author">
+   Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, and George Candea
+ </div>
+ 
+ <h2>Abstract:</h2>
+ <blockquote>
+ Symbolic execution is a powerful technique for analyzing program behavior, finding bugs, and generating tests, but suffers from severely limited scalability: the largest programs that can be symbolically executed today are on the order of thousands of lines of code. To ensure feasibility of symbolic execution, even small programs must curtail their interactions with libraries, the operating system, and hardware devices. This paper introduces selective symbolic execution, a technique for creating the illusion of full-system symbolic execution, while symbolically running only the code that is of interest to the developer. We describe a prototype that can symbolically execute arbitrary portions of a full system, including applications, libraries, operating system, and device drivers. It seamlessly transitions back and forth between symbolic and concrete execution, while transparently converting system state from symbolic to concrete and back. Our technique makes symbolic exec!
 ution practical for large software that runs in real environments, without requiring explicit modeling of these environments.
+ </blockquote>
+ 
+ <h2>Published:</h2>
+ <blockquote>
+   "Selective Symbolic Execution"
+   <br>
+   Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, and George Candea.
+   <br>
+ <i>
+ Fifth Workshop on Hot Topics in System Dependability
+ </i>, Lisbon, Portugal, June 2009.
+ </blockquote>
+ <h2>Download:</h2>
+ <h3>Paper:</h3>
+ <ul>
+   <li><a href="2009-06-HotDep-SymbolicExec.pdf">
+   Selective Symbolic Execution
+   </a> (PDF)</li>
+ </ul>
+ 
+ <!-- *********************************************************************** -->
+ <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/2009-06-HotDep-SymbolicExec.pdf


Index: llvm-www/pubs/pubs.js
diff -u llvm-www/pubs/pubs.js:1.49 llvm-www/pubs/pubs.js:1.50
--- llvm-www/pubs/pubs.js:1.49	Thu Aug 20 12:18:35 2009
+++ llvm-www/pubs/pubs.js	Sun Sep 20 12:02:16 2009
@@ -25,6 +25,14 @@
    month: 6,
    year: 2009},
 
+  {url: '2009-06-HotDep-SymbolicExec.html',
+   title: 'Selective Symbolic Execution',
+   author: 'Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, and George Candea',
+   published: "Proc. Fifth Workshop on Hot Topics in System Dependability (HotDep'09)",
+   location: "Lisbon, Portugal",
+   month: 6,
+   year: 2009},
+
   {url: '2009-06-27-edwin.html',
    title: 'Interprocedural bounds checker for C programs using symbolic constraints and slicing',
    author: 'Edvin Török',






More information about the llvm-commits mailing list