Awesome
A bibliography of papers related to symbolic execution
The following list was earlier hosted at https://sites.google.com/site/symexbib/. From now on, the plan is to update only this list.
The list is a bit out of date since I have not added many papers since 2013. But I would love to keep it up to date. If you want to add any paper to the list, please send a pull request or email me (http://www.cs.stanford.edu/~saswat).
| Title | Venue | Year | Authors |
|---|---|---|---|
| Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing | VMCAI | 2015 | Maria Christakis, Patrice Godefroid |
| Dynamic Test Generation with Static Fields and Initializers | RV | 2014 | Maria Christakis, Patrick Emmisberger, Peter Müller |
| Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations | SEFM | 2014 | Maria Christakis, Peter Müller, Valentin Wüstholz |
| Enhancing Symbolic Execution with Veritesting | ICSE | 2014 | Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, David Brumley |
| Prototyping Symbolic Execution Engines for Interpreted Languages | ASPLOS | 2014 | Stefan Bucur, Johannes Kinder, George Candea |
| Finding Trojan Message Vulnerabilities in Distributed Systems | ASPLOS | 2014 | 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 | Chaoqiang Zhang, Alex Groce, Mohammad Amin Alipour |
| Enhancing Symbolic Execution with Built-In Term Rewriting and Constrained Lazy Initialization | FSE | 2013 | P. Braione, G. Denaro, M. Pezzè |
| AppIntent: analyzing sensitive data transmission in android for privacy leakage detection | CCS | 2013 | Zhemin Yang, Min Yang, Yuan Zhang, Guofei Gu,Peng Ning, X. Sean Wang |
| Z3-str: a z3-based string solver for web application analysis | FSE | 2013 | Yunhui Zheng, Xiangyu Zhang, Vijay Ganesh |
| An orchestrated survey of methodologies for automated software test case generation | Journal of Systems and Software | 2013 | Saswat Anand, Edmund Burke, Tsong Yueh Chen, John Clark, Myra B. Cohen, Wolfgang Grieskamp, Mark Harman, Mary Jean Harrold, Phil McMinn |
| Verifying systems rules using rule-directed symbolic execution | ASPLOS | 2013 | Heming Cui, Gang Hu, Jingyue Wu, and Junfeng Yang |
| Symbolic Execution for Software Testing: Three Decades Later | CACM | 2013 | Cristian Cadar and Koushik Sen. |
| Boosting concolic testing via interpolation | FSE | 2013 | 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 | |
| Explicating symbolic execution (xSymExe): an evidence-based verification framework | ICSE | 2013 | John Hatcliff, Robby, Patrice Chalin, and Jason Belt |
| Memoise: A tool for memoized symbolic execution | ICSE | 2013 | Guowei Yang, Sarfraz Khurshid, and Corina S. Păsăreanu |
| Billions and Billions of Constraints: Whitebox Fuzz Testing in Production | ICSE | 2013 | Ella Bounimova, Patrice Godefroid, David Molnar |
| Feedback-directed unit test generation for C/C++ using concolic execution | ICSE | 2013 | Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, and Aarti Gupta |
| Reliability analysis in symbolic pathfinder | ICSE | 2013 | Antonio Filieri, Corina S. Păsăreanu, and Willem Visser |
| Input-covering schedules for multithreaded programs | OOPSLA | 2013 | Tom Bergan, Luis Ceze, and Dan Grossman |
| Steering symbolic execution to less traveled paths | OOPSLA | 2013 | You Li, Zhendong Su, Linzhang Wang, and Xuandong Li |
| A Generic Framework for Symbolic Execution | SLE | 2013 | Andrei Arusoaie, Dorel Lucanu, Vlad Rusu |
| Symbiotic: Synergy of instrumentation, slicing, and symbolic execution | TACAS | 2013 | Jiri Slaby, Jan Strejček, Marek Trtík |
| SmacC: A Retargetable Symbolic Execution Engine | TACAS | 2013 | Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr |
| Path exploration based on symbolic output | TOSEM | 2013 | Dawei Qi, Hoang D. T. Nguyen, and Abhik Roychoudhury |
| Redundant State Detection for Dynamic Symbolic Execution | USENIX | 2013 | Suhabe Bugrara, Dawson Engler |
| Augmented dynamic symbolic execution | ASE | 2012 | Konrad Jamrozik, Gordon Fraser, Nikolai Tillmann and Jonathan de Halleux |
| Collaborative Verification and Testing with Explicit Assumptions | FM | 2012 | Maria Christakis, Peter Müller, Valentin Wüstholz |
| Automated Concolic Testing of Smartphone Apps | FSE | 2012 | Saswat Anand, Mayur Naik, Hongseok Yang, Mary Jean Harrold |
| Data Races vs. Data Race Bugs: Telling the Difference with Portend | ASPLOS | 2012 | Baris Kasikci, Cristian Zamfir, George Candea |
| TRACER: A Symbolic Execution Tool for Verification | CAV | 2012 | Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa |
| Computational verification of C protocol implementations by symbolic execution | CCS | 2012 | Mihhail Aizatulin, Andrew D. Gordon, and Jan Jürjens |
| Integration testing of software product lines using compositional symbolic execution | FASE | 2012 | Jiangfan Shi, Myra B. Cohen, Matthew B. Dwyer |
| Rubicon: bounded verification of web applications | FSE | 2012 | Joseph P. Near and Daniel Jackson |
| Green: reducing, reusing and recycling constraints in program analysis | FSE | 2012 | Willem Visser, Jaco Geldenhuys, and Matthew B. Dwyer |
| make test-zesti: A Symbolic Execution Solution for Improving Regression Testing | ICSE | 2012 | Paul Dan Marinescu, Cristian Cadar |
| A Scalable Distributed Concolic Testing Approach: An Empirical Evaluation | ICST | 2012 | Moonzoo Kim, Yunho Kim, Gregg Rothermel |
| Symbolic Execution with Interval Solving and Meta-heuristic Search | ICST | 2012 | Mateus Borges, Marcelo d’Amorim, Saswat Anand, David Bushnell, Corina S. Pasareanu |
| Probabilistic symbolic execution | ISSTA | 2012 | Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser |
| Memoized symbolic execution | ISSTA | 2012 | Guowei Yang, Corina S. Păsăreanu, and Sarfraz Khurshid |
| Higher-order symbolic execution via contracts | OOPSLA | 2012 | Sam Tobin-Hochstadt and David Van Horn |
| Scaling symbolic execution using ranged analysis | OOPSLA | 2012 | Junaid Haroon Siddiqui and Sarfraz Khurshid |
| Symdrive: testing drivers without devices | OSDI | 2012 | Matthew J. Renzelmann, Asim Kadav, and Michael M. Swift |
| Efficient state merging in symbolic execution | PLDI | 2012 | Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea |
| GKLEE: concolic verification and test generation for GPUs | PPoPP | 2012 | Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, and Sreeranga P. Rajan |
| Loop invariant symbolic execution for parallel programs | VMCAI | 2012 | Stephen F. Siegel, and Timothy K. Zirkel |
| Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs | ASE | 2011 | Saswat Anand, Mary Jean Harrold |
| S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems | ASPLOS | 2011 | Vitaly Chipounov, Volodymyr Kuznetsov, George Candea |
| LCT: An Open Source Concolic Testing Tool for Java Programs | Bytecode | 2011 | 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 | Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, V. N. Venkatakrishnan |
| Symbolic Crosschecking of Floating-Point and SIMD Code | EuroSys | 2011 | Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly |
| Parallel Symbolic Execution for Automated Real-World Software Testing | EuroSys | 2011 | Stefan Bucur, Vlad Ureche, Cristian Zamfir, George Candea |
| Theoretical aspects of compositional symbolic execution | FASE | 2011 | 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 | Christoph Csallner, Leonidas Fegaras, Chengkai Li |
| Camouflage: Automated Anonymization of Field Data | ICSE | 2011 | James Clause, Alex Orso |
| Precise Identification of Problems for Structural Test Generation | ICSE | 2011 | Xusheng Xiao, Tao Xie, Nikolai Tillmann, Jonathan de Halleux |
| Symbolic Execution for Software Testing in Practice -- Preliminary Assessment | ICSE Impact Project Focus Area | 2011 | Christian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina Pasareanu, Koushik Sen, Nikolai Tillmann, Willem Visser |
| Lazy symbolic execution for test data generation | IET Software | 2011 | M.X. Lin, Y.L. Chen, K. Yu, G.S. Wu |
| Statically-Directed Dynamic Automated Test Generation | ISSTA | 2011 | Domagoj Babic, Lorenzo Martignoni, Stephen McCamant, Dawn Song |
| Automatic Partial Loop Summarization in Dynamic Test Generation | ISSTA | 2011 | Patrice Godefroid, Daniel Luchaup |
| Symbolic Execution with Mixed Concrete-Symbolic Solving | ISSTA | 2011 | Corina Pasareanu, Neha Rungta, Willem Visser |
| Selecting peers for execution comparison | ISSTA | 2011 | William N. Sumner, Tao Bao, Xiangyu Zhang |
| eXpress: Guided Path Exploration for Efficient Regression Test Generation | ISSTA | 2011 | Kunal Taneja, Tao Xie, Nikolai Tillmann, Jonathan De Halleux |
| Path-based Inductive Synthesis for Program Inversion | PLDI | 2011 | Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, Jeffrey S. Foster |
| kb-Anonymity: A Model for Anonymized Behavior-Preserving Test and Debugging Data | PLDI | 2011 | Aditya Budi, David Lo, Lingxiao Jiang, Lucia |
| Higher-Order Test Generation | PLDI | 2011 | Patrice Godefroid |
| Directed Incremental Symbolic Execution | PLDI | 2011 | 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 | Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa |
| Directed Symbolic Execution | SAS | 2011 | 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 | 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 | Prithvi Bisht, A. Prasad Sistla, V. N. Venkatakrishnan | |
| Symbolic PathFinder: symbolic execution of Java bytecode | ASE | 2010 | Corina S. Păsăreanu, Neha Rungta |
| Solving string constraints lazily | ASE | 2010 | Pieter Hooimeijer, Westley Weimer |
| Abstract Analysis of Symbolic Executions | CAV | 2010 | Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik |
| JReq: Database Queries in Imperative Languages | CC | 2010 | Ming-Yee Iu, Emmanuel Cecchet, Willy Zwaenepoel |
| Input generation via decomposition and re-stitching: finding bugs in Malware | CCS | 2010 | Juan Caballero, Pongsin Poosankam, Stephen McCamant, Domagoj Babi ć, Dawn Song |
| Symbolic Security Analysis of Ruby-on-Rails Web Applications | CCS | 2010 | Avik Chaudhuri, Jeffrey S. Foster |
| Privacy-preserving genomic computation through program specialization | CCS | 2010 | 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 | Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, Radoslaw Bobrowicz, V. N. Venkatakrishnan |
| Reverse engineering of binary device drivers with RevNIC | EuroSys | 2010 | Vitaly Chipounov, George Candea |
| HadoopToSQL: a mapReduce query optimizer | EuroSys | 2010 | Ming-Yee Iu, Willy Zwaenepoel |
| Execution Synthesis: A Technique for Automated Software Debugging | EuroSys | 2010 | Cristian Zamfir, George Candea |
| Directed test suite augmentation: techniques and tradeoffs | FSE | 2010 | Zhihong Xu, Yunho Kim, Moonzoo Kim, Gregg Rothermel, Myra B. Cohen |
| Using symbolic evaluation to understand behavior in configurable software systems | ICSE | 2010 | 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 | Kiran Lakhotia, Nikolai Tillmann, Mark Harman, Jonathan De Halleux |
| Is Data Privacy Always Good for Software Testing? | ISSRE | 2010 | Mark Grechanik, Christoph Csallner, Chen Fu, Qing Xie |
| Exploiting program dependencies for scalable multiple-path symbolic execution | ISSTA | 2010 | Raul Santelices, Mary Jean Harrold |
| Directed Test Generation for Effective Fault Localization | ISSTA | 2010 | Shay Artzi, Julian Dolby, Frank Tip, Marco Pistoi |
| Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis | ISSTA | 2010 | Patrice Godefroid, Johannes Kinder |
| Parallel symbolic execution for structural test generation | ISSTA | 2010 | 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 | Kiran Lakhotia, Phil McMinn, Mark Harman |
| Systematic Testing for Control Applications | MemoCODE | 2010 | Rupak Majumdar, Indranil Saha, Zilong Wang |
| Mixing type checking and symbolic execution | PLDI | 2010 | Yit Phang Khoo, Bor-Yuh Evan Chang, Jeffrey S. Foster |
| Program Analysis via Satisfiability Modulo Path Programs | POPL | 2010 | William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta |
| Compositional may-must program analysis: unleashing the power of alternation | POPL | 2010 | Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, Sai Deep Tetali |
| Experimental comparison of concolic and random testing for java card applets | SPIN | 2010 | Kari Kähkönen, Roland Kindermann, Keijo Heljanko, Ilkka Niemelä |
| Toward Automated Detection of Logic Vulnerabilities in Web Applications | USENIX Security | 2010 | Viktoria Felmetsger, Ludovico Cavedon, Christopher Kruegel, Giovanni Vigna |
| Dynamic symbolic database application testing | Workshop on Testing Database Systems | 2010 | Chengkai Li, Christoph Csallner |
| Reggae: Automated Test Generation for Programs Using Complex Regular Expressions | ASE | 2009 | Nuo Li, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, Wolfram Schulte |
| Looper: Lightweight Detection of Infinite Loops at Runtime | ASE | 2009 | Jacob Burnim, Nicholas Jalbert, Christos Stergiou, Koushik Sen |
| Reducing Test Inputs Using Information Partitions | CAV | 2009 | |
| Symbolic Query Exploration | Formal Methods and Software Engineering | 2009 | Margus Veanes, Pavel Grigorenko, Peli Halleux, Nikolai Tillmann |
| Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses | FSE | 2009 | Jason Belt, Robby, Xianghua Deng |
| Darwin: an approach for debugging evolving programs | FSE | 2009 | Dawei Qi, Abhik Roychoudhury, Zhenkai Liang, Kapil Vaswani |
| Symbolic Query Exploration | ICFEM | 2009 | |
| 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 | Jacob Burnim, Sudeep Juvekar, Koushik Sen |
| Automatic creation of SQL Injection and cross-site scripting attacks | ICSE | 2009 | Adam Kieyzun, Philip J. Guo, Karthick Jayaraman, Michael D. Ernst |
| Euclide: A Constraint-Based Testing Framework for Critical C Programs | ICST | 2009 | Arnaud Gotlieb |
| Fitness-guided path exploration in dynamic symbolic execution | International Conference on Dependable Systems and Networks | 2009 | |
| Discovering Application-Level Insider Attacks Using Symbolic Execution | International Information Security Conference | 2009 | |
| Precise pointer reasoning for dynamic test generation | ISSTA | 2009 | Bassem Elkarablieh, Patrice Godefroid, Michael Y. Levin |
| HAMPI: a solver for string constraints | ISSTA | 2009 | 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 | William G.J. Halfond, Saswat Anand, Alessandro Orso |
| Loop-extended symbolic execution on binary programs | ISSTA | 2009 | |
| IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution | Network and Distributed System Security Symposium | 2009 | Tielei Wang, Tao Wei, Zhiqiang Lin, Wei Zou |
| Cloud9: a software testing service | Operating Systems Review | 2009 | |
| Snugglebug: a powerful approach to weakest preconditions | PLDI | 2009 | |
| Symbolic Robustness Analysis | RTSS | 2009 | Rupak Majumdar, Indranil Saha |
| State Joining and Splitting for the Symbolic Execution of Binaries | Runtime Verification | 2009 | Trevor Hansen, Peter Schachte, Harald Søndergaard |
| Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution | SPIN | 2009 | |
| A survey of new trends in symbolic execution for software testing and analysis | STTT | 2009 | Corina S. Păsăreanu, Willem Visser |
| Symbolic execution with abstraction | STTT | 2009 | Saswat Anand, Corina S. Păsăreanu, Willem Visser |
| Test Input Generation for Programs with Pointers | TACAS | 2009 | 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 | David Molnar, Xue Cong Li, David A. Wagner |
| Selective Symbolic Execution | Workshop on Hot Topics in System Dependability | 2009 | V. Chipounov, V. Georgescu, C. Zamfir, and G. Candea |
| EXE: Automatically Generating Inputs of Death | ACM Trans. Inf. Syst. Secur. | 2008 | |
| Test-Suite Augmentation for Evolving Software | ASE | 2008 | |
| Heuristics for Scalable Dynamic Test Generation | ASE | 2008 | |
| Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution | Asian Symposium on Programming Languages and Systems | 2008 | |
| Better bug reporting with better privacy | ASPLOS | 2008 | |
| Automatically Identifying Trigger-based Behavior in Malware | Botnet Detection | 2008 | David Brumley, Cody Hartwig, Zhenkai Liang, James Newsome, Dawn Song, Heng Yin |
| Randomized directed testing (REDIRECT) for Simulink/Stateflow models | EMSOFT | 2008 | Manoranjan Satpathy, Anand Yeolekar, S. Ramesh |
| Differential symbolic execution | FSE | 2008 | |
| DySy: dynamic symbolic execution for invariant inference | ICSE | 2008 | |
| Calysto: scalable and precise extended static checking | ICSE | 2008 | |
| Active property checking | International conference on Embedded software | 2008 | |
| Pex-White Box Test Generation for .NET | International Conf. on Tests and Proofs | 2008 | |
| Dynamic Test Input Generation for Web Applications | ISSTA | 2008 | |
| Universal symbolic execution and its application to likely data structure invariant generation | ISSTA | 2008 | |
| Dynamic test input generation for web applications | ISSTA | 2008 | |
| Combining unit-level symbolic execution and system-level concrete execution for testing NASA software | ISSTA | 2008 | |
| Automated Whitebox Fuzz Testing | Network and Distributed System Security Symposium | 2008 | |
| KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs | OSDI | 2008 | |
| Grammar-based whitebox fuzzing | PLDI | 2008 | |
| Using Dynamic Symbolic Execution to Improve Deductive Verification | SPIN | 2008 | |
| RWset: Attacking Path Explosion in Constraint-Based Test Generation | TACAS | 2008 | |
| Demand-Driven Compositional Symbolic Execution | TACAS | 2008 | |
| Combining symbolic execution with model checking to verify parallel numerical programs | TOSEM | 2008 | |
| Vigilante: End-to-End Containment of Internet Worm Epidemics | Transactions on Computer Systems | 2008 | |
| Panalyst: privacy-aware remote error analysis on commodity software | USENIX Security Symposium | 2008 | |
| A Decision Procedure for Bitvectors and Arrays | CAV | 2007 | Ganesh and Dill |
| Directed test generation using symbolic grammars | ASE | 2007 | |
| Creating Vulnerability Signatures Using Weakest Preconditions | Computer Security Foundations Symposium | 2007 | |
| Predictive testing: amplifying the effectiveness of software testing | ESEC/FSE | 2007 | |
| Hybrid Concolic Testing | ICSE | 2007 | |
| Variably interprocedural program analysis for runtime error detection | ISSTA | 2007 | |
| Dynamic test input generation for database applications | ISSTA | 2007 | |
| Compositional dynamic test generation | POPL | 2007 | |
| QAGen: generating query-aware test databases | SIGMOD Conf. | 2007 | Carsten Binnig, Donald Kossmann, Eric Lo, M. Tamer Özsu |
| Bouncer: securing software by blocking bad input | SOSP | 2007 | |
| Exploring Multiple Execution Paths for Malware Analysis | Symposium on Security and Privacy | 2007 | |
| JPF-SE: A Symbolic Execution Extension to Java PathFinder | TACAS | 2007 | Saswat Anand, Corina Pasareanu, Willem Visser |
| Type-Dependence Analysis and Program Transformation for Symbolic Execution | TACAS | 2007 | Saswat Anand, Alex Orso, Mary Jean Harrold |
| BitScope: Automatically Dissecting Malicious Binaries | Technical Report CMU-CS-07-133, School of Computer Science, Carnegie Mellon University | 2007 | |
| Saturn: A scalable framework for error detection using Boolean satisfiability | TOPLAS | 2007 | |
| Towards Automatic Discovery of Deviations in Binary Implementations with Applications to Error Detection and Fingerprint Generation | USENIX Security Symposium | 2007 | David Brumley, Juan Caballero, Zhenkai Liang, James Newsome, Dawn Song |
| EXE: Automatically Generating Inputs of Death | CCS | 2006 | Cadar, Ganesh, Pawlowski, Dill, Engler |
| Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems | ASE | 2006 | Xianghua Deng, Jooyong Lee, Robby |
| Temporal search: detecting hidden malware timebombs with virtual machines | ASPLOS | 2006 | 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 | Koushik Sen, Gul Agha |
| Test input generation for java containers using state matching | ISSTA | 2006 | Willem Visser, Corina S. Pasareanu, Radek Pelánek |
| Symbolic Execution with Abstract Subsumption Checking | Model Checking Software, International SPIN Workshop | 2006 | Saswat Anand, Corina S. Pasareanu, Willem Visser |
| Symbolic execution of floating-point computations | Software Testing, Verification & Reliability | 2006 | Bernard Botella, Arnaud Gotlieb, Claude Michel |
| Automatically Generating Malicious Disks using Symbolic Execution | Symposium on Security and Privacy | 2006 | Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar, Dawson R. Engler |
| MATRIX: Maintenance-Oriented Testing Requirements Identifier and Examiner | TAIC PART | 2006 | Taweesup Apiwattanapong, Raúl A. Santelices, Pavan Kumar Chittimalli, Alessandro Orso, Mary Jean Harrold |
| Test input generation for red-black trees using abstraction | ASE | 2005 | Willem Visser, Corina S. Pasareanu, Radek Pelánek |
| CUTE: a concolic unit testing engine for C | FSE | 2005 | Koushik Sen, Darko Marinov, Gul Agha |
| Generalizing symbolic execution to library classes | PASTE | 2005 | Sarfraz Khurshid, Yuk Lai Suen |
| DART: directed automated random testing | PLDI | 2005 | Patrice Godefroid, Nils Klarlund, Koushik Sen |
| Execution Generated Test Cases: How to Make Systems Code Crash Itself | SPIN | 2005 | Cristian Cadar, Dawson R. Engler |
| Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution | TACAS | 2005 | Tao Xie, Darko Marinov, Wolfram Schulte, David Notkin |
| Automating mimicry attacks using static binary analysis | USENIX Security Symposium | 2005 | Christopher Kruegel, Engin Kirda, Darren Mutz, William K. Robertson, Giovanni Vigna |
| Test input generation with java PathFinder | ISSTA | 2004 | Willem Visser, Corina S. Păsăreanu, Sarfraz Khurshid |
| Verification of Java Programs Using Symbolic Execution and Invariant Generation | Model Checking Software, International SPIN Workshop | 2004 | Corina S. Păsăreanu, Willem Visser |
| Bogor: an extensible and highly-modular software model checking framework | FSE | 2003 | Robby, Matthew B. Dwyer, John Hatcliff |
| Generalized Symbolic Execution for Model Checking and Testing | TACAS | 2003 | Sarfraz Khurshid, Corina S. Păsăreanu, Willem Visser |
| Extended Static Checking for Java | PLDI | 2002 | Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata |
| Bandera: a source-level interface for model checking Java programs | ICSE | 2000 | James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby |
| Symbolic Testing and the DISSECT Symbolic Evaluation System | IEEE Tran. Software Engg. | 1977 | William E. Howden |
| Symbolic Execution and Program Testing | Commun. ACM | 1976 | James C. King |