A Bibliography of Papers on Symbolic Execution Technique and its Applications

This list has moved to: https://github.com/saswatanand/symexbib


The symbolic execution (also known as symbolic evaluation) technique is a specific type of symbolic analysis of programs. Other forms of symbolic analysis of programs include bounded model checking (which tools such as CBMC, ESC/Java use) and abstraction-based model checking (which tools such as SLAM, BLAST use). One distinction between symbolic execution and the other two techniques is that the other techniques encode program's behavior on all program paths under a given bound/abstraction into one gigantic formula, and check its satisfiability. Whereas, symbolic execution analyzes program behavior on one or a subset of paths (using compositional symbolic execution) at a time. Because of this piecemeal nature of symbolic execution, it can be used selectively analyze program behavior on a subset of all program paths of large programs, and thus, it is more suitable for software testing (i.e., to find bugs). In contrast, the other two techniques are more suitable for software verification (i.e., to prove absence of bugs), but they do no scale very well to large programs.

The symbolic execution technique was first proposed in seventies as a technique for automated software testing.  However, in the last decade a great deal of research has focused on (1) using the technique in a wide range of applications (e.g., ensuring software security and privacy, program refactoring, program equivalence checking, fault localization), (2) addressing the technique's fundamental limitations (e.g., path explosion problem, inability to solve complex constraints), and (3) enabling the technique's application to real-world programs written in different programming languages (e.g., C, Java, Javascript, PHP, Ruby).

Following is an attempt to maintain a partial bibliography of papers on symbolic execution published in a wide range of venues. The list of conferences include conferences in software engineering (e.g., ICSE, ASE, FSE, ISSTA, FASE, ISSRE, ICST), systems (e.g., ASPLOS, EusoSys, RTSS), security (e.g., CCS, Oakland Security and Privacy, USENIX Security), software verification (e.g., CAV, TACAS, VMCAI, SPIN), programming languages (e.g., POPL, PLDI, SAS, CC), database (e.g., SIGMOD).

If you know of a paper that is missing from the list or you would like to update the list yourself, please contact me.

Thanks to the following contributors:
  • Amin Alipour
  • Stefan Bucur
Showing 193 items
TitleVenueYearAbstractAuthors
Sort 
 
Sort 
 
Sort 
 
Sort 
 
Sort 
 
TitleVenueYearAbstractAuthors
Prototyping Symbolic Execution Engines for Interpreted Languages ASPLOS 2014 Prototyping Symbolic Execution Engines for Interpreted Languages Stefan Bucur, Johannes Kinder, George Candea 
Finding Trojan Message Vulnerabilities in Distributed Systems ASPLOS 2014 Finding Trojan Message Vulnerabilities in Distributed Systems Radu Banabic, George Candea, Rachid Guerraoui 
How We Get There: A Context-Guided Search Strategy in Concolic Testing  FSE 2014   Hyunmin Seo and Sunghun Kim 
SymJS: Automatic Symbolic Testing of JavaScript Web Applications  FSE 2014   Guodong Li, Esben Andreasen, and Indradeep Ghosh 
Statistical Symbolic Execution with Informed Sampling FSE 2014   Antonio Filieri, Corina S. Păsăreanu, Willem Visser, and Jaco Geldenhuys 
Extending a Search-Based Test Generator with Adaptive Dynamic Symbolic Execution ISSTA 2014   Juan Pablo Galeotti, Gordon Fraser, and Andrea Arcuri 
Using Test Case Reduction and Prioritization to Improve Symbolic Execution ISSTA 2014 Using Test Case Reduction and Prioritization to Improve Symbolic Execution  Chaoqiang Zhang, Alex Groce, Mohammad Amin Alipour 
Verifying systems rules using rule-directed symbolic execution ASPLOS 2013 Verifying systems rules using rule-directed symbolic execution Heming Cui, Gang Hu, Jingyue Wu, and Junfeng Yang 
Symbolic Execution for Software Testing: Three Decades Later CACM 2013 Symbolic execution for software testing: three decades later Cristian Cadar and Koushik Sen. 
Boosting concolic testing via interpolation FSE 2013 Boosting concolic testing via interpolation Joxan Jaffar, Vijayaraghavan Murali, and Jorge A. Navas 
Jalangi: a tool framework for concolic testing, selective record-replay, and dynamic analysis of JavaScript FSE 2013 Jalangi: a tool framework for concolic testing, selective record-replay, and dynamic analysis of JavaScript  
Explicating symbolic execution (xSymExe): an evidence-based verification framework ICSE 2013 Explicating symbolic execution (xSymExe): an evidence-based verification framework John Hatcliff, Robby, Patrice Chalin, and Jason Belt 
Memoise: A tool for memoized symbolic execution ICSE 2013 Memoise: A tool for memoized symbolic execution Guowei Yang, Sarfraz Khurshid, and Corina S. Păsăreanu 
Billions and Billions of Constraints: Whitebox Fuzz Testing in Production ICSE 2013 Billions and Billions of Constraints: Whitebox Fuzz Testing in Production Ella Bounimova, Patrice Godefroid, David Molnar 
Feedback-directed unit test generation for C/C++ using concolic execution ICSE 2013 Feedback-directed unit test generation for C/C++ using concolic execution Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, and Aarti Gupta 
Reliability analysis in symbolic pathfinder ICSE 2013 Reliability analysis in symbolic pathfinder Antonio Filieri, Corina S. Păsăreanu, and Willem Visser 
Input-covering schedules for multithreaded programs OOPSLA 2013 Input-covering schedules for multithreaded programs Tom Bergan, Luis Ceze, and Dan Grossman 
Steering symbolic execution to less traveled paths OOPSLA 2013 Steering symbolic execution to less traveled paths  You Li, Zhendong Su, Linzhang Wang, and Xuandong Li 
A Generic Framework for Symbolic Execution SLE 2013 A Generic Framework for Symbolic Execution Andrei Arusoaie, Dorel Lucanu, Vlad Rusu 
Symbiotic: Synergy of instrumentation, slicing, and symbolic execution TACAS 2013 Symbiotic: Synergy of instrumentation, slicing, and symbolic execution Jiri Slaby, Jan Strejček, Marek Trtík  
SmacC: A Retargetable Symbolic Execution Engine TACAS 2013 SmacC: A Retargetable Symbolic Execution Engine  Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr 
Path exploration based on symbolic output TOSEM 2013 Path exploration based on symbolic output  Dawei Qi, Hoang D. T. Nguyen, and Abhik Roychoudhury 
Redundant State Detection for Dynamic Symbolic Execution USENIX 2013 Redundant State Detection for Dynamic Symbolic Execution Suhabe Bugrara, Dawson Engler 
Augmented dynamic symbolic execution ASE 2012 Augmented dynamic symbolic execution Konrad Jamrozik, Gordon Fraser, Nikolai Tillmann and Jonathan de Halleux 
Data Races vs. Data Race Bugs: Telling the Difference with Portend ASPLOS 2012 Data Races vs. Data Race Bugs: Telling the Difference with Portend Baris Kasikci, Cristian Zamfir, George Candea 
TRACER: A Symbolic Execution Tool for Verification CAV 2012 TRACER: A Symbolic Execution Tool for Verification Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa 
Computational verification of C protocol implementations by symbolic execution CCS 2012 Computational verification of C protocol implementations by symbolic execution Mihhail Aizatulin, Andrew D. Gordon, and Jan Jürjens 
Integration testing of software product lines using compositional symbolic execution FASE 2012 Integration testing of software product lines using compositional symbolic execution Jiangfan Shi, Myra B. Cohen, Matthew B. Dwyer 
Rubicon: bounded verification of web applications FSE 2012 Rubicon: bounded verification of web applications Joseph P. Near and Daniel Jackson 
Green: reducing, reusing and recycling constraints in program analysis FSE 2012 Green: reducing, reusing and recycling constraints in program analysis Willem Visser, Jaco Geldenhuys, and Matthew B. Dwyer 
make test-zesti: A Symbolic Execution Solution for Improving Regression Testing ICSE 2012 make test-zesti: A Symbolic Execution Solution for Improving Regression Testing Paul Dan Marinescu, Cristian Cadar  
A Scalable Distributed Concolic Testing Approach: An Empirical Evaluation ICST 2012 A Scalable Distributed Concolic Testing Approach: An Empirical Evaluation Moonzoo Kim, Yunho Kim, Gregg Rothermel 
Symbolic Execution with Interval Solving and Meta-heuristic Search ICST 2012 Symbolic Execution with Interval Solving and Meta-heuristic Search Mateus Borges, Marcelo d’Amorim, Saswat Anand, David Bushnell, Corina S. Pasareanu  
Probabilistic symbolic execution ISSTA 2012 Probabilistic symbolic execution Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser 
Memoized symbolic execution ISSTA 2012 Memoized symbolic execution Guowei Yang, Corina S. Păsăreanu, and Sarfraz Khurshid 
Higher-order symbolic execution via contracts OOPSLA 2012 Higher-order symbolic execution via contracts Sam Tobin-Hochstadt and David Van Horn 
Scaling symbolic execution using ranged analysis OOPSLA 2012 Scaling symbolic execution using ranged analysis Junaid Haroon Siddiqui and Sarfraz Khurshid 
Symdrive: testing drivers without devices OSDI 2012 Symdrive: testing drivers without devices Matthew J. Renzelmann, Asim Kadav, and Michael M. Swift 
Efficient state merging in symbolic execution PLDI 2012 Efficient state merging in symbolic execution  Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea 
GKLEE: concolic verification and test generation for GPUs PPoPP 2012 GKLEE: concolic verification and test generation for GPUs Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, and Sreeranga P. Rajan 
Loop invariant symbolic execution for parallel programs VMCAI 2012 Loop invariant symbolic execution for parallel programs Stephen F. Siegel, and Timothy K. Zirkel 
Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs ASE 2011 Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs Saswat Anand, Mary Jean Harrold 
S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems ASPLOS 2011 S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems Vitaly Chipounov, Volodymyr Kuznetsov, George Candea 
LCT: An Open Source Concolic Testing Tool for Java Programs Bytecode 2011 LCT: An Open Source Concolic Testing Tool for Java Programs Kähkönen, K., Launiainen, T, Saarikivi, O., Kauttio, J., Heljanko, K., and Niemelä, I. 
KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs CAV 2011  Guodong Li, Indradeep Ghosh, Sreeranga Rajan 
Practical, low-effort verification of real code using under-constrained execution CAV 2011  David Ramos, Dawson Engler 
WAPTEC: whitebox analysis of web applications for parameter tampering exploit construction CCS 2011 WAPTEC: whitebox analysis of web applications for parameter tampering exploit construction Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, V. N. Venkatakrishnan 
Symbolic Crosschecking of Floating-Point and SIMD Code EuroSys 2011 Symbolic Crosschecking of Floating-Point and SIMD Code Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly 
Parallel Symbolic Execution for Automated Real-World Software Testing EuroSys 2011 Parallel Symbolic Execution for Automated Real-World Software Testing Stefan Bucur, Vlad Ureche, Cristian Zamfir, George Candea 
Theoretical aspects of compositional symbolic execution FASE 2011 Theoretical aspects of compositional symbolic execution Dries Vanoverberghe, Frank Piessens 
Testing Software In Age Of Data Privacy: A Balancing Act FSE 2011  Kunal Taneja, Mark Grechanik, Rayid Ghani and Tao Xie 
Path Exploration based on Symbolic Output FSE 2011  Dawei Qi, Hoang D.T. Nguyen, Abhik Roychoudhury 
Testing MapReduce-style programs FSE (New Ideas Track) 2011 Testing MapReduce-style programs Christoph Csallner, Leonidas Fegaras, Chengkai Li 
Camouflage: Automated Anonymization of Field Data ICSE 2011 Camouflage: Automated Anonymization of Field Data James Clause, Alex Orso 
Precise Identification of Problems for Structural Test Generation ICSE 2011 Precise Identification of Problems for Structural Test Generation Xusheng Xiao, Tao Xie, Nikolai Tillmann, Jonathan de Halleux 
Symbolic Execution for Software Testing in Practice -- Preliminary Assessment ICSE Impact Project Focus Area 2011 Symbolic Execution for Software Testing in Practice -- Preliminary Assessment Christian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina Pasareanu, Koushik Sen, Nikolai Tillmann, Willem Visser 
Lazy symbolic execution for test data generation IET Software 2011 Lazy symbolic execution for test data generation M.X. Lin, Y.L. Chen, K. Yu, G.S. Wu  
Statically-Directed Dynamic Automated Test Generation ISSTA 2011 Statically-Directed Dynamic Automated Test Generation Domagoj Babic, Lorenzo Martignoni, Stephen McCamant, Dawn Song 
Automatic Partial Loop Summarization in Dynamic Test Generation ISSTA 2011 Automatic Partial Loop Summarization in Dynamic Test Generation Patrice Godefroid, Daniel Luchaup 
Symbolic Execution with Mixed Concrete-Symbolic Solving ISSTA 2011 Symbolic Execution with Mixed Concrete-Symbolic Solving Corina Pasareanu, Neha Rungta, Willem Visser 
Selecting peers for execution comparison ISSTA 2011 Selecting peers for execution comparison William N. Sumner, Tao Bao, Xiangyu Zhang 
eXpress: Guided Path Exploration for Efficient Regression Test Generation ISSTA 2011 eXpress: Guided Path Exploration for Efficient Regression Test Generation Kunal Taneja, Tao Xie, Nikolai Tillmann, Jonathan De Halleux 
Path-based Inductive Synthesis for Program Inversion PLDI 2011 Path-based Inductive Synthesis for Program Inversion Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, Jeffrey S. Foster 
kb-Anonymity: A Model for Anonymized Behavior-Preserving Test and Debugging Data PLDI 2011 kb-Anonymity: A Model for Anonymized Behavior-Preserving Test and Debugging Data Aditya Budi, David Lo, Lingxiao Jiang, Lucia 
Higher-Order Test Generation PLDI 2011 Higher-Order Test Generation Patrice Godefroid 
Directed Incremental Symbolic Execution PLDI 2011 Directed Incremental Symbolic Execution Suzette Person, Guowei Yang, Neha Rungta, Sarfraz Khurshid 
Automatic Formal Verification of MPI-Based Parallel Programs  PPoPP 2011  Stephen F. Siegel, Timothy K. Zirkel 
Unbounded Symbolic Execution for Program Verification RV 2011 Unbounded Symbolic Execution for Program Verification Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa 
Directed Symbolic Execution SAS 2011 Directed Symbolic Execution Kin-Keung Ma, Yit Phang Khoo, Jeffrey S. Foster, Michael Hicks 
MACE: Model-inference-Assisted Concolic Exploration for Protocol and Vulnerability Discovery USENIX Security 2011 MACE: Model-inference-Assisted Concolic Exploration for Protocol and Vulnerability Discovery Chia Yuan Cho, Domagoj Babić, Pongsin Poosankam, Kevin Zhijie Chen, Edward XueJun Wu, Dawn Song 
Collective Assertions  VMCAI 2011  Stephen F. Siegel, Timothy K. Zirkel 
Automatically Preparing Safe SQL Queries  2010 Automatically Preparing Safe SQL Queries Prithvi Bisht, A. Prasad Sistla, V. N. Venkatakrishnan  
Symbolic PathFinder: symbolic execution of Java bytecode ASE 2010 Symbolic PathFinder: symbolic execution of Java bytecode Corina S. Păsăreanu, Neha Rungta 
Solving string constraints lazily ASE 2010 Solving string constraints lazily Pieter Hooimeijer, Westley Weimer 
Abstract Analysis of Symbolic Executions CAV 2010 Abstract Analysis of Symbolic Executions Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik 
JReq: Database Queries in Imperative Languages CC 2010 JReq: Database Queries in Imperative Languages Ming-Yee Iu, Emmanuel Cecchet, Willy Zwaenepoel 
Input generation via decomposition and re-stitching: finding bugs in Malware CCS 2010 Input generation via decomposition and re-stitching: finding bugs in Malware Juan Caballero, Pongsin Poosankam, Stephen McCamant, Domagoj Babi ć, Dawn Song 
Symbolic Security Analysis of Ruby-on-Rails Web Applications  CCS 2010 Symbolic Security Analysis of Ruby-on-Rails Web Applications Avik Chaudhuri, Jeffrey S. Foster 
Privacy-preserving genomic computation through program specialization CCS 2010 Privacy-preserving genomic computation through program specialization Rui Wang, XiaoFeng Wang, Zhou Li, Haixu Tang, Michael K. Reiter, Zheng Dong 
NoTamper: Automatic Blackbox Detection of Parameter Tampering Opportunities in Web Applications CCS 2010 NoTamper: Automatic Blackbox Detection of Parameter Tampering Opportunities in Web Applications Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, Radoslaw Bobrowicz, V. N. Venkatakrishnan 
Reverse engineering of binary device drivers with RevNIC EuroSys 2010 Reverse engineering of binary device drivers with RevNIC Vitaly Chipounov, George Candea 
HadoopToSQL: a mapReduce query optimizer EuroSys 2010 HadoopToSQL: a mapReduce query optimizer Ming-Yee Iu, Willy Zwaenepoel  
Execution Synthesis: A Technique for Automated Software Debugging EuroSys 2010 Execution Synthesis: A Technique for Automated Software Debugging Cristian Zamfir, George Candea 
Directed test suite augmentation: techniques and tradeoffs FSE 2010 Directed test suite augmentation: techniques and tradeoffs Zhihong Xu, Yunho Kim, Moonzoo Kim, Gregg Rothermel, Myra B. Cohen 
Using symbolic evaluation to understand behavior in configurable software systems ICSE 2010 Using symbolic evaluation to understand behavior in configurable software systems. Elnatan Reisner, Charles Song, Kin-Keung Ma, Jeffrey S. Foster, Adam Porter 
FloPSy: search-based floating point constraint solving for symbolic execution Intl Conf on Testing software and systems 2010 FloPSy: search-based floating point constraint solving for symbolic execution Kiran Lakhotia, Nikolai Tillmann, Mark Harman, Jonathan De Halleux 
Is Data Privacy Always Good for Software Testing? ISSRE 2010 Is Data Privacy Always Good for Software Testing? Mark Grechanik, Christoph Csallner, Chen Fu, Qing Xie 
Exploiting program dependencies for scalable multiple-path symbolic execution ISSTA 2010 Exploiting program dependencies for scalable multiple-path symbolic execution Raul Santelices, Mary Jean Harrold 
Directed Test Generation for Effective Fault Localization ISSTA 2010 Directed Test Generation for Effective Fault Localization Shay Artzi, Julian Dolby, Frank Tip, Marco Pistoi 
Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis ISSTA 2010 Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis Patrice Godefroid, Johannes Kinder 
Parallel symbolic execution for structural test generation ISSTA 2010 Parallel symbolic execution for structural test generation Matt Staats, Corina Pǎsǎreanu 
An empirical investigation into branch coverage for C programs using CUTE and AUSTIN Journal of Systems and Software 2010 An empirical investigation into branch coverage for C programs using CUTE and AUSTIN Kiran Lakhotia, Phil McMinn, Mark Harman 
Systematic Testing for Control Applications MemoCODE 2010 Systematic Testing for Control Applications Rupak Majumdar, Indranil Saha, Zilong Wang  
Mixing type checking and symbolic execution PLDI 2010 Mixing type checking and symbolic execution Yit Phang Khoo, Bor-Yuh Evan Chang, Jeffrey S. Foster 
Program Analysis via Satisfiability Modulo Path Programs POPL 2010 Program Analysis via Satisfiability Modulo Path Programs William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta 
Compositional may-must program analysis: unleashing the power of alternation POPL 2010 Compositional may-must program analysis: unleashing the power of alternation Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, Sai Deep Tetali 
Experimental comparison of concolic and random testing for java card applets SPIN 2010 Experimental comparison of concolic and random testing for java card applets Kari Kähkönen, Roland Kindermann, Keijo Heljanko, Ilkka Niemelä 
Toward Automated Detection of Logic Vulnerabilities in Web Applications USENIX Security 2010 Toward Automated Detection of Logic Vulnerabilities in Web Applications Viktoria Felmetsger, Ludovico Cavedon, Christopher Kruegel, Giovanni Vigna 
Dynamic symbolic database application testing Workshop on Testing Database Systems 2010 Dynamic symbolic database application testing Chengkai Li, Christoph Csallner 
Reggae: Automated Test Generation for Programs Using Complex Regular Expressions ASE 2009 Reggae: Automated Test Generation for Programs Using Complex Regular Expressions Nuo Li, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, Wolfram Schulte 
Looper: Lightweight Detection of Infinite Loops at Runtime ASE 2009 Looper: Lightweight Detection of Infinite Loops at Runtime Jacob Burnim, Nicholas Jalbert, Christos Stergiou, Koushik Sen 
Reducing Test Inputs Using Information Partitions CAV 2009 http://dblp.uni-trier.de/rec/bibtex/conf/cav/MajumdarX09  
Symbolic Query Exploration Formal Methods and Software Engineering 2009 Symbolic Query Exploration Margus Veanes, Pavel Grigorenko, Peli Halleux, Nikolai Tillmann 
Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses FSE 2009 Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses Jason Belt, Robby, Xianghua Deng 
Darwin: an approach for debugging evolving programs FSE 2009 Darwin: an approach for debugging evolving programs Dawei Qi, Abhik Roychoudhury, Zhenkai Liang, Kapil Vaswani 
Symbolic Query Exploration ICFEM 2009 Symbolic Query Exploration  
Event Listener Analysis and Symbolic Execution for Testing GUI Applications ICFEM 2009  Svetoslav R. Ganov, Chip Killmar, Sarfraz Khurshid, Dewayne E. Perry 
WISE: Automated test generation for worst-case complexity ICSE 2009 WISE: Automated test generation for worst-case complexity Jacob Burnim, Sudeep Juvekar, Koushik Sen 
Automatic creation of SQL Injection and cross-site scripting attacks ICSE 2009 Automatic creation of SQL Injection and cross-site scripting attacks Adam Kieyzun, Philip J. Guo, Karthick Jayaraman, Michael D. Ernst 
Euclide: A Constraint-Based Testing Framework for Critical C Programs ICST 2009 Euclide: A Constraint-Based Testing Framework for Critical C Programs Arnaud Gotlieb 
Fitness-guided path exploration in dynamic symbolic execution International Conference on Dependable Systems and Networks 2009 http://dblp.uni-trier.de/rec/bibtex/conf/dsn/XieTHS09  
Discovering Application-Level Insider Attacks Using Symbolic Execution International Information Security Conference 2009 Discovering Application-Level Insider Attacks Using Symbolic Execution  
Precise pointer reasoning for dynamic test generation ISSTA 2009 Precise pointer reasoning for dynamic test generation Bassem Elkarablieh, Patrice Godefroid, Michael Y. Levin 
HAMPI: a solver for string constraints ISSTA 2009 HAMPI: a solver for string constraints Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst 
Precise interface identification to improve testing and analysis of web applications ISSTA 2009 Precise interface identification to improve testing and analysis of web applications William G.J. Halfond, Saswat Anand, Alessandro Orso 
Loop-extended symbolic execution on binary programs ISSTA 2009 Loop-extended symbolic execution on binary programs  
IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution Network and Distributed System Security Symposium 2009 IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution Tielei Wang, Tao Wei, Zhiqiang Lin, Wei Zou 
Cloud9: a software testing service Operating Systems Review 2009 http://dblp.uni-trier.de/rec/bibtex/journals/sigops/CiorteaZBCC09  
Snugglebug: a powerful approach to weakest preconditions PLDI 2009 Snugglebug: a powerful approach to weakest preconditions  
Symbolic Robustness Analysis RTSS 2009 Symbolic Robustness Analysis Rupak Majumdar, Indranil Saha  
State Joining and Splitting for the Symbolic Execution of Binaries Runtime Verification 2009 State Joining and Splitting for the Symbolic Execution of Binaries Trevor Hansen, Peter Schachte, Harald Søndergaard 
Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution SPIN 2009 http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/v/Visser:Willem.html  
A survey of new trends in symbolic execution for software testing and analysis STTT 2009 A survey of new trends in symbolic execution for software testing and analysis Corina S. Păsăreanu, Willem Visser 
Symbolic execution with abstraction STTT 2009 Symbolic execution with abstraction Saswat Anand, Corina S. Păsăreanu, Willem Visser 
Test Input Generation for Programs with Pointers TACAS 2009 Test Input Generation for Programs with Pointers Dries Vanoverberghe, Nikolai Tillmann, Frank Piessens 
 TACAS 2009 Path Feasibility Analysis for String-Manipulating Programs  
Dynamic Test Generation To Find Integer Bugs in x86 Binary Linux Programs USENIX Security Symposium 2009 Dynamic Test Generation To Find Integer Bugs in x86 Binary Linux Programs David Molnar, Xue Cong Li, David A. Wagner 
Selective Symbolic Execution Workshop on Hot Topics in System Dependability 2009 Selective Symbolic Execution V. Chipounov, V. Georgescu, C. Zamfir, and G. Candea 
EXE: Automatically Generating Inputs of Death ACM Trans. Inf. Syst. Secur. 2008 EXE: Automatically Generating Inputs of Death  
Test-Suite Augmentation for Evolving Software ASE 2008 http://dblp.uni-trier.de/rec/bibtex/conf/kbse/SantelicesCAOH08  
Heuristics for Scalable Dynamic Test Generation ASE 2008 http://dblp.uni-trier.de/rec/bibtex/conf/kbse/BurnimS08  
Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution Asian Symposium on Programming Languages and Systems 2008 http://dblp.uni-trier.de/rec/bibtex/conf/aplas/LiSGORK08  
Better bug reporting with better privacy ASPLOS 2008 Better bug reporting with better privacy  
Automatically Identifying Trigger-based Behavior in Malware Botnet Detection 2008 Automatically Identifying Trigger-based Behavior in Malware David Brumley, Cody Hartwig, Zhenkai Liang, James Newsome, Dawn Song, Heng Yin 
Randomized directed testing (REDIRECT) for Simulink/Stateflow models EMSOFT 2008 Randomized directed testing (REDIRECT) for Simulink/Stateflow models Manoranjan Satpathy, Anand Yeolekar, S. Ramesh 
Differential symbolic execution FSE 2008 Differential symbolic execution  
DySy: dynamic symbolic execution for invariant inference ICSE 2008 DySy: dynamic symbolic execution for invariant inference  
Calysto: scalable and precise extended static checking ICSE 2008 Calysto: scalable and precise extended static checking  
Active property checking International conference on Embedded software 2008 Active property checking  
Pex-White Box Test Generation for .NET International Conf. on Tests and Proofs 2008 Pex-White Box Test Generation for .NET  
Dynamic Test Input Generation for Web Applications ISSTA 2008 Dynamic Test Input Generation for Web Applications  
Universal symbolic execution and its application to likely data structure invariant generation ISSTA 2008 http://dblp.uni-trier.de/rec/bibtex/conf/issta/KannanS08  
Dynamic test input generation for web applications ISSTA 2008 Dynamic test input generation for web applications  
Combining unit-level symbolic execution and system-level concrete execution for testing NASA software ISSTA 2008 Combining unit-level symbolic execution and system-level concrete execution for testing NASA software  
Automated Whitebox Fuzz Testing Network and Distributed System Security Symposium 2008 Automated Whitebox Fuzz Testing  
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs OSDI 2008 KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs  
Grammar-based whitebox fuzzing PLDI 2008 Grammar-based whitebox fuzzing  
Using Dynamic Symbolic Execution to Improve Deductive Verification SPIN 2008 http://dblp.uni-trier.de/rec/bibtex/conf/spin/VanoverbergheBHST08  
RWset: Attacking Path Explosion in Constraint-Based Test Generation TACAS 2008 RWset: Attacking Path Explosion in Constraint-Based Test Generation  
Demand-Driven Compositional Symbolic Execution TACAS 2008 Demand-Driven Compositional Symbolic Execution  
Combining symbolic execution with model checking to verify parallel numerical programs TOSEM 2008 http://dblp.uni-trier.de/rec/bibtex/journals/tosem/SiegelMAC08  
Vigilante: End-to-End Containment of Internet Worm Epidemics Transactions on Computer Systems 2008 Vigilante: End-to-End Containment of Internet Worm Epidemics  
Panalyst: privacy-aware remote error analysis on commodity software USENIX Security Symposium  2008 Panalyst: privacy-aware remote error analysis on commodity software  
Directed test generation using symbolic grammars ASE 2007 Directed test generation using symbolic grammars  
A Decision Procedure for Bitvectors and Arrays CAV 2007 A Decision Procedure for Bitvectors and Arrays Vijay Ganesh and David L. Dill 
Creating Vulnerability Signatures Using Weakest Preconditions Computer Security Foundations Symposium 2007 Creating Vulnerability Signatures Using Weakest Preconditions  
Predictive testing: amplifying the effectiveness of software testing ESEC/FSE 2007 Predictive testing: amplifying the effectiveness of software testing  
Hybrid Concolic Testing ICSE 2007 http://dblp.uni-trier.de/rec/bibtex/conf/icse/MajumdarS07  
Variably interprocedural program analysis for runtime error detection ISSTA 2007 Variably interprocedural program analysis for runtime error detection  
Dynamic test input generation for database applications ISSTA 2007 http://dblp.uni-trier.de/rec/bibtex/conf/issta/EmmiMS07  
Compositional dynamic test generation POPL 2007 Compositional dynamic test generation  
QAGen: generating query-aware test databases SIGMOD Conf. 2007 QAGen: generating query-aware test databases Carsten Binnig, Donald Kossmann, Eric Lo, M. Tamer Özsu 
Bouncer: securing software by blocking bad input SOSP 2007 Bouncer: securing software by blocking bad input  
Exploring Multiple Execution Paths for Malware Analysis Symposium on Security and Privacy 2007 Exploring Multiple Execution Paths for Malware Analysis  
JPF-SE: A Symbolic Execution Extension to Java PathFinder TACAS 2007 JPF-SE: A Symbolic Execution Extension to Java PathFinder  
Type-Dependence Analysis and Program Transformation for Symbolic Execution TACAS 2007 Type-Dependence Analysis and Program Transformation for Symbolic Execution  
BitScope: Automatically Dissecting Malicious Binaries Technical Report CMU-CS-07-133, School of Computer Science, Carnegie Mellon University 2007 BitScope: Automatically Dissecting Malicious Binaries  
Saturn: A scalable framework for error detection using Boolean satisfiability TOPLAS 2007 http://dblp.uni-trier.de/rec/bibtex/journals/toplas/XieA07  
Towards Automatic Discovery of Deviations in Binary Implementations with Applications to Error Detection and Fingerprint Generation USENIX Security Symposium 2007 Towards Automatic Discovery of Deviations in Binary Implementations with Applications to Error Detection and Fingerprint Generation David Brumley, Juan Caballero, Zhenkai Liang, James Newsome, Dawn Song 
Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems ASE 2006 Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems  
Temporal search: detecting hidden malware timebombs with virtual machines ASPLOS 2006 Temporal search: detecting hidden malware timebombs with virtual machines Jedidiah R. Crandall, Gary Wassermann, Daniela A. S. de Oliveira, Zhendong Su, Shyhtsun Felix Wu, Frederic T. Chong 
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools CAV 2006 CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools  
EXE: Automatically Generating Inputs of Death CCS 2006 EXE: Automatically Generating Inputs of Death Cristian Cadar, Vijay Ganesh, Peter Pawlowski, Dawson Engler, and David L. Dill 
Test input generation for java containers using state matching ISSTA 2006 Test input generation for java containers using state matching  
Symbolic Execution with Abstract Subsumption Checking Model Checking Software, International SPIN Workshop 2006 Symbolic Execution with Abstract Subsumption Checking  
Symbolic execution of floating-point computations Software Testing, Verification & Reliability 2006 Symbolic execution of floating-point computations  
Automatically Generating Malicious Disks using Symbolic Execution Symposium on Security and Privacy 2006 Automatically Generating Malicious Disks using Symbolic Execution  
MATRIX: Maintenance-Oriented Testing Requirements Identifier and Examiner TAIC PART 2006 MATRIX: Maintenance-Oriented Testing Requirements Identifier and Examiner  
Test input generation for red-black trees using abstraction ASE 2005 Test input generation for red-black trees using abstraction  
CUTE: a concolic unit testing engine for C FSE 2005 CUTE: a concolic unit testing engine for C  
Generalizing symbolic execution to library classes PASTE 2005 Generalizing symbolic execution to library classes  
DART: directed automated random testing PLDI 2005 DART: directed automated random testing  
Execution Generated Test Cases: How to Make Systems Code Crash Itself SPIN 2005 Execution Generated Test Cases: How to Make Systems Code Crash Itself  
Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution TACAS 2005 Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution  
Automating mimicry attacks using static binary analysis USENIX Security Symposium 2005 Automating mimicry attacks using static binary analysis  
Test input generation with java PathFinder ISSTA 2004 Test input generation with java PathFinder  
Verification of Java Programs Using Symbolic Execution and Invariant Generation Model Checking Software, International SPIN Workshop 2004 Verification of Java Programs Using Symbolic Execution and Invariant Generation  
Bogor: an extensible and highly-modular software model checking framework FSE 2003 Bogor: an extensible and highly-modular software model checking framework  
Generalized Symbolic Execution for Model Checking and Testing TACAS 2003 Generalized Symbolic Execution for Model Checking and Testing  
Extended Static Checking for Java PLDI 2002 Extended Static Checking for Java  
Bandera: a source-level interface for model checking Java programs ICSE 2000 Bandera: a source-level interface for model checking Java programs  
Symbolic Testing and the DISSECT Symbolic Evaluation System IEEE Tran. Software Engg. 1977 http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/h/Howden:William_E=.html  
Symbolic Execution and Program Testing Commun. ACM 1976 Symbolic Execution and Program Testing  
Showing 193 items
Comments