This list has moved to: https://github.com/saswatanand/symexbib 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:
|
A Bibliography of Papers on Symbolic Execution Technique and its Applications
| Title | Venue | Year | Abstract | Authors |
|---|---|---|---|---|
| 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