Symbolic Execution

Surveys (Another Bibliography):

• Symbolic Execution for Software Testing in Practice -- Preliminary Assessment. Christian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina Pasareanu, Koushik Sen, Nikolai Tillmann, Willem Visser ICSE 2011 Impact Focused Area.
• All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but might have been afraid to ask),Edward J. Schwartz, Thanassis Avgerinos, David Brumley. (PDF Slides) IEEE Symposium on Security and Privacy. 2010
• A survey of new trends in symbolic execution for software testing and analysis. C. S. Pasareanu and W. Visser. STTT 2009.
• Symbolic Execution and Model Checking for Testing, Corina S. Pasareanu, Willem Visser, Haifa Verification Conference 2007
• Formal Software Analysis: Emerging Trends in Software Model Checking (invited), Matthew B. Dwyer, John Hatcliff, Robby, Corina S. Pasareanu, Willem Visser, ICSE/FOSE 2007.

Search-based Testing:

• Slides on Search Based Test Case Generation by Paolo Tonella (slides 96- are on DSE and its integration with search-based testing)
• CREST Open Workshop Search Based Software Testing (SBST) and Dynamic Symbolic Execution (DSE)
  • Juan Pablo Galeotti, Gordon Fraser, Andrea Arcuri: Improving search-based test suite generation with dynamic symbolic execution. ISSRE 2013. [pdf]
  • Jan Malburg, Gordon Fraser. Combining search‐based and constraint-­based testing. ASE 2011. [pdf]
  • Arthur I. Baars, Mark Harman, Youssef Hassoun, Kiran Lakhotia, Phil McMinn, Paolo Tonella, Tanja E. J. Vos. Symbolic search-­based testing. ASE 2011. [pdf]
  • Tao Xie, Nikolai Tillmann, Jonathan de Halleux, Wolfram Schulte. Fitness-­guided path exploration in dynamic symbolic execution. DSN 2009. [PDF][Slides]
  • Kobi Inkumsah, Tao Xie. Improving Structural Testing of Object-­‐Oriented Programs via Integrating Evolutionary Testing and Symbolic Execution. ASE 2008. [PDF][Slides]

Path Explosion:

• Path Pruning/Prioritization
• Path Exploration based on Symbolic Output. Dawei Qi, Hoang D.T. Nguyen, Abhik Roychoudhury. ESEC/FSE 2011.
  • Statically-Directed Dynamic Automated Test Generation. Domagoj Babic, Lorenzo Martignoni, Stephen McCamant, Dawn Song. ISSTA 2011
  • eXpress: Guided Path Exploration for Efficient Regression Test Generation. Kunal Taneja, Tao Xie, Nikolai Tillmann, and Jonathan de Halleux. ISSTA 2011.
  • Directed Symbolic Execution. Kin-Keung Ma, Yit Phang Khoo, Jeffrey S. Foster, and Michael Hicks. SAS 2011.
  • S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems. Vitaly Chipounov, Volodymyr Kuznetsov, George Candea. ASPLOS 2011.
• Exploiting Program Dependencies for Scalable Multiple-Path Symbolic Execution Raul Santelices and Mary Jean Harrold ISSTA 2010
  • IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution. Tielei Wang, Tao Wei, Zhiqiang Lin, Wei Zou. NDSS 2009.
• Pruning the Search Space in Path-based Test Generation S´ebastien Bardin Philippe Herrmann ICST 2009
• Selective Symbolic Execution Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, and George Candea. HotDep 2009
• Reducing Test Inputs Using Information Partitions Rupak Majumdar and Ru-Gang Xu CAV 2009.
  • Fitness-guided path exploration in dynamic symbolic execution. Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte. DSN 2009.
  • Heuristics for Scalable Dynamic Test Generation. J. Burnim and K. Sen. ASE 2008. [tr]
• RWset: Attacking Path Explosion in Constraint-Based Test Generation Cristian Cadar, Peter Boonstoppel, Dawson Engler TACAS 2008.
  • Exploring Multiple Execution Paths for Malware Analysis. Andreas Moser, Christopher Kruegel, and Engin Kirda. Oakland 2007.
• Hybrid Concolic Testing R. Majumdar, K. Sen ICSE 2007
• Partial Instrumentation (Partial Symbolization, Input Region Partition)
  • Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs (slides)
  • Saswat Anand, Mary Jean Harrold. ASE 2011.
• Automatically Identifying Critical Input Regions and Code in Applications Michael Carbin and Martin Rinard ISSTA 2010
• Binary Code Extraction and Interface Identification for Security Applications. Juan Caballero, Noah M. Johnson, Stephen McCamant, and Dawn Song. NDSS 2010.
• Taint-based directed whitebox fuzzing, Ganesh, Vijay and Leek, Tim and Rinard, Martin, ICSE 2009
  • WISE: Automated Test Generation for Worst-Case Complexity Jacob Burnim, Sudeep Juvekar, Koushik Sen, ICSE 2009
• Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution. Xin Li, Daryl Shannon, Indradeep Ghosh, Mizuhito Ogawa, Sreeranga P. Rajan, Sarfraz Khurshid. APLAS 2008.
• Type-Dependence Analysis and Program Transformation for Symbolic Execution. Saswat Anand, Alessandro Orso and Mary Jean Harrold. TACAS 2007.
• Compositional (summary-based)
  • Higher-Order Test Generation. Patrice Godefroid. PLDI 2011.
  • Theoretical aspects of compositional symbolic execution. Dries Vanoverberghe, Frank Piessens. FASE 2011.
  • Compositional may-must program analysis: unleashing the power of alternation. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, Sai Deep Tetali. POPL 2010.
  • Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation, Patrice Godefroid, Shuvendu K. Lahiri, and Cindy Rubio-Gonzalez. MSR-TR-2010-11
  • Demand-Driven Compositional Symbolic Execution Saswat Anand, Patrice Godefroid2, and Nikolai Tillmann. TACAS 2008
  • Compositional Dynamic Test Generation Patrice Godefroid. POPL 2007.
  • Saturn: A scalable framework for error detection using Boolean satisfiability. Yichen Xie, Alex Aiken. TOPLAS 2007.
  • Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. X. Deng, J. Lee, and Robby. ASE 2006.
  • Software Partitioning for Effective Automated Unit Testing EMSOFT 2006.
  • Generalizing Symbolic Execution to Library Classes. S. Khurshid and Y. Suen. PASTE 2005.
• State abstraction
  • MACE: Model-inference-Assisted Concolic Exploration for Protocol and Vulnerability Discovery. Chia Yuan Cho, Domagoj Babic, Pongsin Poosankam, Kevin Zhijie Chen, Dawn Song and Edward XueJun Wu. USENIX Security 2011.
  • Symbolic Execution with Abstraction, Saswat Anand, Corina S. Pasareanu, Willem Visser, STTT, 2009
  • Cloud9: a software testing service. Liviu Ciortea, Cristian Zamfir, Stefan Bucur, Vitaly Chipounov, George Candea. Operating Systems Review 2009.
  • State Joining and Splitting for the Symbolic Execution of Binaries. Trevor Hansen, Peter Schachte, Harald Søndergaard. RV 2009.
  • Test input generation for java containers using state matching. W. Visser, C. Pasareanu, and R. Pelanek. ISSTA 2006.
  • Symbolic Execution with Abstract Subsumption Checking, Saswat Anand, Corina S. Pasareanu, Willem Visser, SPIN 2006.
  • Execution generated test cases: How to make systems code crash itself (invited paper). C. Cadar and D. Engler. SPIN’05,
  • Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. Tao Xie, Darko Marinov, Wolfram Schulte, and David Notkin. TACAS 2005.
• Parallelism
  • Parallel Symbolic Execution for Automated Real-World Software Testing. Stefan Bucur, Vlad Ureche, Cristian Zamfir, George Candea. EuroSys 2011.
• Parallel Symbolic Execution for Structural Test Generation Matt Staats and Corina Pasareanu ISSTA 2010
• ParSym: Parallel symbolic execution. J. H. Siddiqui and S. Khurshid. ICSTE’10,
• Scalable distributed concolic testing: a case study on a flash storage platform. Y. Kim, M. Kim, and N. Dang. ICTAC’10.
• Constraint solving optimization/static analysis
  • Enhancing Symbolic Execution with Built-In Term Rewriting and Constrained Lazy Initialization. P. Braione, G. Denaro, M. Pezzè. ESEC/FSE 2013.
  • Symbolic Execution with Interval Constraint Solving and Meta-heuristic Search
    • Mateus Borges, Marcelo d'Amorim, Saswat Anand, David Bushnell, Corina Pasareanu. ICST 2012.
    • Symbolic Execution with Mixed Concrete-Symbolic Solving, C. Pasareanu, N. Rungta, and W. Visser. ISSTA 2011.
    • Coral: Solving complex constraints for symbolic pathfinder. M. Souza, M. Borges, M. d’Amorim, and C. P˘as˘areanu. NFM’11.
  • Optimizing Constraint Solving to Better Support Symbolic Execution. I. Erete and A. Orso. CSTVA 2011.
    • Mixing type checking and symbolic execution. Yit Phang Khoo, Bor-Yuh Evan Chang, Jeffrey S. Foster. PLDI 2010.
  • Flopsy - search-based floating point constraint solving for symbolic execution. K. Lakhotia, N. Tillmann, M. Harman, and J. de Halleux. ICTSS’10.
  • Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses, Belt, Jason and Robby, and Deng, Xianghua, FSE 2009
  • Klee: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. Cristian Cadar, Daniel Dunbar, Dawson Engler. OSDI 2008.
    • Calysto: scalable and precise extended static checking. Domagoj Babi\'c and Alan J. Hu. ICSE 2008.
    • Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software, C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, M. Pape. ISSTA 2008
  • CUTE: a concolic unit testing engine for C. Koushik Sen and Darko Marinov and Gul Agha. FSE 2005.
  • DART: directed automated random testing. Patrice Godefroid and Nils Klarlund and Koushik Sen. PLDI 2005
    • Floating Points:
      • Symbolic Crosschecking of Floating-Point and SIMD Code. Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly. ISSTA 2011.
    • Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis Patrice Godefroid and Johannes Kinder ISSTA 2010
      • Symbolic execution of floating-point computations. Bernard Botella. Arnaud Gotlieb. Claude Michel. STVR 06.
    • Pointers:
      • Test Input Generation for Programs with Pointers. Dries Vanoverberghe, Nikolai Tillmann, Frank Piessens. TACAS 2009.
      • Precise pointer reasoning for dynamic test generation. Bassem Elkarablieh, Patrice Godefroid, Michael Y. Levin. ISSTA 2009.

Loops:

• Recent papers by Marek Trtík
  • Managing Performance vs. Accuracy Trade-offs With Loop Perforation. S.Sidiroglou, S.Misailovic, H.Hoffmann, M.Rinard. ESEC/FSE 2011.
  • Symbolic Execution for Verification . J. Jaffar, J. A. Navas, A. E. Santosa. Unpublished (old) Draft 2011.
  • Simplifying Loop Invariant Generation Using Splitter Predicates. Rahul Sharma, Isil Dillig, Thomas Dillig, and Alex Aiken. CAV 2011.
  • Detecting and Escaping Infinite Loops with Jolt. Michael Carbin, Sasa Misailovic, Michael Kling, and Martin Rinard. ECOOP 2011.
  • Automatic Partial Loop Summarization in Dynamic Test Generation. Patrice Godefroid Daniel Luchaup. ISSTA'2011
  • Refining the Control Structure of Loops using Static Analysis, Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic and Aarti Gupta. EMSOFT 2009
  • Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities , Richard M. Chang, Franjo Ivancic, Geoff Jiang, Sriram Sankaranarayanan and Vitaly Shmatikov. CSF 2009.
  • Looper: Lightweight Detection of Infinite Loops at Runtime. Jacob Burnim, Nicholas Jalbert, Christos Stergiou, Koushik Sen. ASE 2009
  • WISE: Automated Test Generation for Worst-Case Complexity Jacob Burnim, Sudeep Juvekar, Koushik Sen, ICSE 2009 [paper] [slides] [benchmarks]
• Loop-Extended Symbolic Execution on Binary Programs. Prateek Saxena, Pongsin Poosankam, Stephen McCamant, and Dawn Song. ISSTA 2009.
• DySy: Dynamic Symbolic Execution for Invariant Inference. Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis. ICSE 2008.
• Testing for Buffer Overflows with Length Abstraction. Ru-Gang Xu and Rupak Majumdar. ISSTA 2008.

Regression Testing

• AUTOMATED REGRESSION TESTING AND VERIFICATION OF COMPLEX CODE CHANGES. MARCEL BOHME. Dissertation. NUS 2014.
• Verification-Aided Regression Testing. Fabrizio Pastore, Leonardo Mariani, Antti Hyvarinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehestedt, and Ali Muhammad. ISSTA 2014.
• COVRIG: A Framework for the Analysis of Code, Test, and Coverage Evolution in Real Software. Paul Marinescu, Petr Hosek, Cristian Cadar. ISSTA 2014.
• CoREBench: Studying Complexity of Regression Errors. Marcel Böhme, Abhik Roychoudhury. ISSTA 2014.
• Property differencing for incremental checking. Guowei Yang, Sarfraz Khurshid, Suzette Person, and Neha Rungta. ICSE 2014.
• Patch verification via multiversion interprocedural control flow graphs. Wei Le and Shannon D. Pattison. ICSE 2014.
• Shadow symbolic execution for better testing of evolving software. Cristian Cadar and Hristina Palikareva. ICSE NIER 2014.
• Hybrid Directed Test Suite Augmentation: An Interleaving Framework. Y. Kim, Z. Xu, M. Kim, M. B. Cohen, G. Rothermel. ICST 2014.
• Regression tests to expose change interaction errors. Marcel Böhme, Bruno C. d. S. Oliveira, and Abhik Roychoudhury. ESEC/FSE 2013.
• KATCH: High-Coverage Testing of Software Patches. Paul Dan Marinescu, Cristian Cadar. ESEC/FSE 2013.
  • Expressing and checking intended changes via software change contracts. Jooyong Yi, Dawei Qi, Shin Hwei Tan, Abhik Roychoudhury. ISSTA 2013.
• Partition-based regression verification. Marcel Böhme, Bruno C. d. S. Oliveira, Abhik Roychoudhury. ICSE 2013.
• Safe Software Updates via Multi-version Execution. Petr Hosek, Cristian Cadar. ICSE 2013.
• make test-zesti: A Symbolic Execution Solution for Improving Regression Testing. Paul Dan Marinescu, Cristian Cadar. ICSE 2012.
• High-Coverage Symbolic Patch Testing. Paul Dan Marinescu, Cristian Cadar. SPIN 2012.
• Path Exploration based on Symbolic Output. Dawei Qi, Hoang D.T. Nguyen, Abhik Roychoudhury. ESEC/FSE 2011.
• A Hybrid Directed Test Suite Augmentation Technique. Z. Xu, Y. Kim, M. Kim, G. Rothermel. ISSRE 2011.
  • Practical, low-effort verification of real code. David Ramos and Dawson Engler. CAV 2011.
  • Differential Slicing: Identifying Causal Execution Differences for Security Applications. Noah Johnson, Juan Caballero, Kevin Zhijie Chen, Stephen McCamant,Pongsin Poosankam, Daniel Reynaud, Dawn Song. Oakland 2011.
  • eXpress: Guided Path Exploration for Efficient Regression Test Generation. Kunal Taneja, Tao Xie, Nikolai Tillmann, and Jonathan de Halleux. ISSTA 2011.
  • Change-Aware Preemption Prioritization. V. Jagannath, Q. Luo, and D. Marinov. ISSTA 2011.
  • Symbolic Crosschecking of Floating-Point and SIMD Code. Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly. ISSTA 2011.
• Directed Incremental Symbolic Execution. S. Person, G. Yang, N. Rungta, and S. Khurshid. PLDI 2011
  • A Security Policy Oracle: Detecting Security Holes Using Multiple API Implementations. Varun Srivastava, Michael D. Bond, Kathryn S. McKinley, Vitaly Shmatikov. PLDI 2011.
• Applying Aggressive Propagation-based Strategies for Testing Changes. Raul Santelices and Mary Jean Harrold. ICST 2011. [slides]
  • Validating Changes and Upgrades in Networked Software. Analysis of evolution of the state of the art in academia andindustry. 2010. [Project web]
• Directed test suite augmentation: techniques and tradeoffs. Z. Xu, Y. Kim, M. Kim, G. Rothermel, and M. B. Cohen. FSE’10,
• Golden Implementation Driven Software Debugging. Ansuman Banerjee, Abhik Roychoudhury, Johannes A. Harlie, Zhenkai Liang. FSE 2010.
  • Test Generation to Expose Changes in Evolving Programs. Dawei Qi, Abhik Roychoudhury, Zhenkai Liang. ASE 2010.
• "Probabilistic Slicing for Predictive Impact Analysis". Raul Santelices and Mary Jean Harrold. Technical report GIT-CERCS-10-10,
• "Exploiting Program Dependencies for Scalable Multiple-path Symbolic Execution". Raul Santelices and Mary Jean Harrold. ISSTA 2010. [slides]
• "Precisely Detecting Runtime Change Interactions for Evolving Software". Raul Santelices, Mary Jean Harrold, and Alessandro Orso. ICST 2010 [slides]
  • Darwin: an approach for debugging evolving programs. Dawei Qi, Abhik Roychoudhury, Zhenkai Liang, Kapil Vaswani. ESEC/FSE 2009.
  • Delta execution for efficient state-space exploration of object-oriented programs. M. d'Amorim, S. Lauterburg, and D. Marinov. TSE 2008.
  • Incremental state-space exploration for programs with dynamically allocated data. S. Lauterburg, A. Sobeih, D. Marinov, and M. Viswanathan. ICSE 2008.
• Differential Symbolic Execution. Suzette Person and Matthew B. Dwyer and Sebastian G. Elbaum and Corina S. Pasareanu. FSE 2008.
• Test-suite Augmentation for Evolving Software. Raul Santelices, Pavan Kumar Chittimalli, Taweesup Apiwattanapong, Alessandro Orso, and Mary Jean Harrold. ASE 2008.
  • Testing Software Product Lines Using Incremental Test Generation. E. Uzuncaova, D. Garcia, S. Khurshid, and D. Batory. ISSRE 2008.
  • 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. USENIX Security 2007.
  • Towards a framework for differential unit testing of object-oriented programs. T. Xie, K. Taneja, S. Kale, and D. Marinov. AST 2007.
• MaTRIX Maintenance-Oriented Test Requirements Identifier and Examiner. T. Apiwattanapong, R. Santelices, P. K. Chittimalli, A. Orso, and M. J. Harrold. TAIC-PART 2006. (Partial Symbolic Execution)

Privacy Preserving

• Partial Replay of Long-Running Applications. Alvin Cheung, Armando Solar-Lezama, Samuel Madden. ESEC/FSE 2011.
• Testing Software In Age Of Data Privacy: A Balancing Act. ESEC/FSE 2011. Kunal Taneja, Mark Grechanik, Rayid Ghani, and Tao Xie.
  • kb-Anonymity: A Model for Anonymized Behavior-Preserving Test and Debugging Data, Aditya BUDI, David LO, Lingxiao JIANG, and Lucia. PLDI 2011. [Slides]
  • Execution Hijacking: Improving Dynamic Analysis by Flying off Course. P. Tsankov, W. Jin, A. Orso, and S. Sinha. ICST 2011.
  • Camouflage: Automated Anonymization of Field Data. J. Clause and A. Orso. ICSE 2011.
  • Is data privacy always good for software testing? by Mark Grechanik, Christoph Csallner, Chen Fu, and Qing Xie. ISSRE 2010.
  • Profile-guided program simplification for effective testing and analysis. Lingxiao Jiang, Zhendong Su. SIGSOFT FSE 2008
  • Better bug reporting with better privacy. M. Castro, M. Costa, J-P. Martin. ASPLOS 2008.
  • Panalyst: Privacy-Aware Remote Error Analysis on Commodity Software. Rui Wang, XiaoFeng Wang, Zhuowei Li. USENIX 2008.

Debugging:

• Generating Range Fixes for Software Configuration. Xiong, Y., A. Hubaux, S. She, and K. Czarnecki. ICSE 2012.
• Differential Slicing: Identifying Causal Execution Differences for Security Applications. Noah Johnson, Juan Caballero, Kevin Zhijie Chen, Stephen McCamant,Pongsin Poosankam, Daniel Reynaud, Dawn Song. Oakland 2011.
• Bug-Assist: Assisting Fault Localization in ANSI-C Programs. Manu Jose and Rupak Majumdar. CAV 2011. [Project web]
• Cause Clue Clauses: Error Localization Using Maximum Satisfiablity. Manu Jose and Rupak Majumdar. PLDI 2011. [Project web]
• Angelic Debugging. Satish Chandra, Emina Torlak, Shaon Barman and Ras Bodik. ICSE 2011. [Slides][Source code]
• Patching Vulnerabilities with Sanitization Synthesis. Fang Yu, Muath Alkhalaf and Tevfik Bultan. ICSE 2011.
• Automated Error Localization and Correction for. Imperative Programs. Robert Könighofer and Roderick Bloem. FMCAD 2011. [slides][project web]
• When does my program fail? J. Rößler, A. Orso, and A. Zeller. CSTVA 2011.
• Execution synthesis: A technique for automated software debugging. C. Zamfir and G. Candea. EuroSys’10.
• Kleenet: automatic bug hunting in sensor network applications. R. Sasnauskas, J. A. B. Link, M. H. Alizai, and K. Wehrle. IPSN’10.
• Golden Implementation Driven Software Debugging. Ansuman Banerjee, Abhik Roychoudhury, Johannes A. Harlie, Zhenkai Liang. FSE 2010.
• Directed Test Generation for Effective Fault Localization. Shay Artzi Julian Dolby Frank Tip Marco Pistoia, ISSTA 2010.
  • On Test Repair using Symbolic Execution. B. Daniel, T. Gvero, and D. Marinov. ISSTA 2010.
• Practical Fault Localization for Dynamic Web Applications. Shay Artzi Julian Dolby Frank Tip Marco Pistoia, ICSE 2010.
• Dynamic symbolic data structure repair. Ishtiaque Hussain and Christoph Csallner. ICSE 2010 NIER
  • Darwin: an approach for debugging evolving programs. Dawei Qi, Abhik Roychoudhury, Zhenkai Liang, Kapil Vaswani. ESEC/FSE 2009.
  • Snugglebug: a powerful approach to weakest preconditions. Satish Chandra, Stephen J. Fink, Manu Sridharan. PLDI 2009.
• Finding Bugs in Dynamic Web Applications. Artzi, Shay; Kiezun, Adam; Dolby, Julian; Tip, Frank; Dig, Danny; Paradkar, Amit; Ernst, Michael D. ISSTA 2008.
• DSDSR: A tool that uses dynamic symbolic execution for data structure repair. by Ishtiaque Hussain and Christoph Csallner. WODA 2008.
  • Vigilante: End-to-End Containment of Internet Worm Epidemics. M. Costa, J. Crowcroft, M. Castro, A.I.T. Rowstron, L. Zhou, L. Zhang, and P. Barham. TCS 2008.
• Creating Vulnerability Signatures Using Weakest Pre-conditions. David Brumley, Hao Wang, Somesh Jha, and Dawn Song. CSFS 2007.
  • Bouncer: securing software by blocking bad input. Miguel Castro. Manuel Costa, Lidong Zhou,. Lintao Zhang, and Marcus Peinado. SOSP 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. USENIX Security 2007.
• Automated Path Generation for Software Fault Localization. Tao Wang and Abhik Roychoudhury. ASE 2005.

Infeasible Code Detection

• TRACER: A Symbolic Execution Tool for Verification. Joxan Jaffar, Vijayaraghavan Murali, Jorge Navas and Andrew Santosa. [Project web]
• A Framework for Path Sensitive Program Analysis, Joxan Jaffar, Vijayaraghavan Murali, Jorge Navas and Andrew Santosa. [Project web]
• Infeasible Basis Paths Detection of Program with Exception-Handling Constructs. Yanmei Zhang, Shujuan Jiang, Qingtan Wang, Xuefeng Zhao. IJACT 2012.
• Joogie: Infeasible Code Detection for Java. Martin Schäf and Stephan Arlt. [Source code]
• Infeasible Code Detection - with Cristiano Bertolini, and Pascal Schweitzer. VSTTE 2012 [Source code]
• IPEG: Utilizing infeasible paths. M. Delahaye. CSTVA 2011.
• Enhancing structural software coverage by incrementally computing branch executability. Mauro Baluda and Pietro Braione and Giovanni Denaro and Mauro Pezzè. Software Quality Journal 2011.
• Automatic structural testing with abstraction refinement and coarsening. Mauro Baluda. SIGSOFT FSE 2011 Doc Sym
• Research on Infeasible Branch-Based Infeasible Path in Program. Pan Lili, Wang Tiane, Qin Jiaohua. IJDCTA 2011.
• Structural coverage of feasible code. Mauro Baluda, Pietro Braione, Giovanni Denaro, Mauro Pezzè. AST 2010.
• Doomed Program Points - J. Hoenicke, R. Leino, A. Podelski, M. Schäf, and T. Wies. FMSD 2010
• A Symbolic Execution Tool Based on the Elimination of Infeasible Paths. Mike Papadakis, Nicos Malevris. ICSEA 2010
• Explanation-Based Generalization of Infeasible Path. Mickaël Delahaye, Bernard Botella, Arnaud Gotlieb. ICST 2010. [Slides]
  • It's doomed; we can prove it - J. Hoenicke, R. Leino, A. Podelski, M. Schäf, and T. Wies. FM 2009 [Source code]
  • Automatic detection of infeasible pathsin software testing. D. Gong, X. Yao. IET 2009.
  • Automatic Determination of Branch Correlations in Software Testing. Dunwei Gong; Xiangjuan Yao; Min Xia. WCSE 2009.
  • Heuristics-based infeasible path detection for dynamic test data generation. Minh Ngoc Ngo, Hee Beng Kuan Tan. IST 2008.
  • Under-constrained execution: making automatic code destruction easy and scalable. Dawson R. Engler, Daniel Dunbar. ISSTA 2007
  • Efficient Detection and Exploitation of Infeasible Paths for Software Timing Analysis. Vivy Suhendra, Tulika Mitra, Abhik Roychoudhury, and Ting Chen. DAC 2006.

Inference:

• Inference and Analysis of Formal Models of Botnet Command and Control Protocols. Chia Yuan Cho, Domagoj Babic, Richard Shin and Dawn Song. CCS 2010.
• Precise Interface Identification to Improve Testing and Analysis of Web Applications. W. Halfond, S. Anand, and A. Orso. ISSTA 2009.
• Universal Symbolic Execution and its Application to Likely Data Structure Invariant Generation. Y. Kannan and K. Sen. ISSTA 2008.
• DySy: Dynamic symbolic execution for invariant inference. Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis. ICSE 2008.
• Using Dynamic Symbolic Execution to Improve Deductive Verification. D. Vanoverberghe, N. Bjørner, J.D. Halleux, W. Schulte, and N. Tillmann. SPIN 2008.
• BitScope: Automatically Dissecting Malicious Binaries. David Brumley, Cody Hartwig, Min Gyung Kang, Zhenkai Liang James Newsome, Pongsin Poosankam, Dawn Song, and Heng Yin. 2007 Technical Report CMU-CS-07-133, School of Computer Science, Carnegie Mellon University

Structured Input Generation:

• Profile-guided program simplification for effective testing and analysis, Jiang, Lingxiao and Su, Zhendong, FSE 2008
  • Test Generation through Programming in UDITA. M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak, and D. Marinov. ICSE 2010.
  • Directed test generation using symbolic grammars. Rupak Majumdar, Ru-gang Xu. ASE 2007.
• Files:
  • Taint-based directed whitebox fuzzing, Ganesh, Vijay and Leek, Tim and Rinard, Martin, ICSE 2009
    • Dynamic Test Generation To Find Integer Bugs in x86 Binary Linux Programs. David Molnar, Cong Li, David A. Wagner. USENIX Security 2009.
  • jFuzz: A concolic whitebox fuzzer for Java. K. Jayaraman, D. Harvison, V. Ganesh, and A. Kiezun. NFM’09.
    • Grammar-based whitebox fuzzing. Patrice Godefroid, Adam Kiezun, Michael Y. Levin. PLDI 2008.
  • Automated Whitebox Fuzz Testing M. Y. Levin P. Godefroid and D.Molnar NDSS 2008
  • Towards Automatic Reverse Engineering of Software Security Configuration. Rui Wang, XiaoFeng Wang, Kehuan Zhang and Zhuowei Li. CCS 2008.
• Strings
  • A Symbolic Execution Framework for JavaScript. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, Dawn Song, Oakland, 2010
    • Solving string constraints lazily. Pieter Hooimeijer and Westley Weimer. ASE 2010.
    • Input generation via decomposition and re-stitching: finding bugs in Malware. Juan Caballero, Pongsin Poosankam, Stephen McCamant, Domagoj Babi ć, Dawn Song. CCS 2010.
  • Hampi: A Solver for String Constraints Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. ISSTA 2009
  • Path feasibility analysis for string-manipulating programs. N. Bjørner, N. Tillmann, and A. Voronkov. TACAS’09,
  • Generating Vulnerability Signatures for String Manipulating Programs Using Automata-based Forward and Backward Symbolic Analyses.", Fang Yu, Muath Alkhalaf and Tevfik Bultan. Short paper. ASE 2009.
    • Reggae: Automated Test Generation for Programs Using Complex Regular Expressions. N. Li, T. Xie, N. Tillmann, J.D. Halleux, and W. Schulte. ASE 2009.
    • Towards Generating High Coverage Vulnerability-Based Signatures with Protocol-Level Constraint-Guided Exploration. Juan Caballero, Zhenkai Liang, Pongsin Poosankam and Dawn Song. RAID 2009.
    • Abstracting Symbolic Execution with String Analysis. D. Shannon, S. Hajra, A. Lee, D. Zhan, and S. Khurshid.TAIC-PART 2007.

Environments:

• Validating Changes and Upgrades in Networked Software. Analysis of evolution of the state of the art in academia andindustry. 2010. [Project web]
• Precise Identification of Problems for Structural Test Generation. Xusheng Xiao, Tao Xie, Nikolai Tillmann, Jonathan de Halleux. ICSE 2011.
• Moles: Tool-assisted environment isolation with closures. J. de Halleux and N. Tillmann. TOOLS’10,
• Automated Environment Generation for Software Model Checking, Oksana Tkachuk, Matthew Dwyer, Corina S. Pasareanu, ASE 2003.
• Database Applications:
  • JReq: Database Queries in Imperative Languages. Ming-Yee Iu, Emmanuel Cecchet, Willy Zwaenepoel. CC 2010.
  • Automatically Preparing Safe SQL Queries. Prithvi Bisht, A. Prasad Sistla, V. N. Venkatakrishnan.
  • HadoopToSQL: a mapReduce query optimizer. Ming-Yee Iu, Willy Zwaenepoel, EuroSys 2010.
  • Analysis & detection of sql injection vulnerabilities via automatic test case generation of programs. M. Ruse, T. Sarkar, and S. Basu IEEE/IPSJ Int. Sym. Applications and the Internet 2010.
  • Dsc+Mock: A test case + mock class generator in support of coding against interfaces. Mainul Islam and Christoph Csallner. WODA 2010.
  • Dynamic symbolic database application testing. Chengkai Li and Christoph Csallner. DBTest 2010.
  • Symbolic Query Exploration. Margus Veanes, Pavel Grigorenko, Peli de Halleux, and Nikolai Tillmann. ICFEM 2009.
  • Dynamic Test Input Generation for Database Applications. M. Emmi, R. Majumdar, and K. Sen. ISSTA 2007.
  • QAGen: generating query-aware test databases. Carsten Binnig, Donald Kossmann, Eric Lo, M. Tamer Özsu. SIGMOD 2007.
• Network/Filesystem Applications:
  • Kleenet: automatic bug hunting in sensor network applications. R. Sasnauskas, J. A. B. Link, M. H. Alizai, and K. Wehrle. IPSN’10.
  • Testing closed-source binary device drivers with DDT. V. Kuznetsov, V. Chipounov, and G. Candea. USENIX ATC’10,
  • Scalable distributed concolic testing: a case study on a flash storage platform. Y. Kim, M. Kim, and N. Dang. ICTAC’10.
    • Reverse engineering of binary device drivers with RevNIC. Vitaly Chipounov, George Candea. EuroSys 2010.
    • Using symbolic evaluation to understand behavior in configurable software systems. Elnatan Reisner, Charles Song, Kin-Keung Ma, Jeffrey S. Foster, Adam Porter. ICSE 2010.
  • Automatically Generating Malicious Disks using Symbolic Execution. Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar and Dawson Engler. Oakland 2006.
  • EXE: Automatically Generating Inputs of Death, Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler. CCS 2006.
• Web Applications?:

===============

Web Applications:

• A Framework for Automated Testing of JavaScript Web Applications Shay Artzi, Julian Dolby, Simon Holm Jensen, Anders Møller and Frank Tip, ICSE 2011
  • NoTamper: Automatic Blackbox Detection of Parameter Tampering Opportunities in Web Applications. Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, Radoslaw Bobrowicz, V. N. Venkatakrishnan . CCS 2010. [Results]
  • Symbolic Security Analysis of Ruby-on-Rails Web Applications. Avik Chaudhuri, Jeffrey S. Foster. CCS 2010.
• Practical Fault Localization for Dynamic Web Applications. Shay Artzi Julian Dolby Frank Tip Marco Pistoia, ICSE 2010.
  • Precise Interface Identification to Improve Testing and Analysis of Web Applications. W. Halfond, S. Anand, and A. Orso. ISSTA 2009.
  • Automatic creation of SQL injection and cross-site scripting attacks. Adam Kieżun, Philip J. Guo, Karthick Jayaraman, and Michael D. Ernst. ICSE 2009.
• Finding Bugs in Dynamic Web Applications. Artzi, Shay; Kiezun, Adam; Dolby, Julian; Tip, Frank; Dig, Danny; Paradkar, Amit; Ernst, Michael D. ISSTA 2008.

Security:

• A Security Policy Oracle: Detecting Security Holes Using Multiple API Implementations. Varun Srivastava, Michael D. Bond, Kathryn S. McKinley, Vitaly Shmatikov. PLDI 2011.
• AEG: Automatic exploit generation. T. Avgerinos, S. K. Cha, B. L. T. Hao, and D. Brumley. NDSS’11
• Discovering Application-Level Insider Attacks Using Symbolic Execution. Karthik Pattabiraman, Nithin Nakka, Zbigniew Kalbarczyk, Ravishankar K. Iyer. IISC 2009.
• Automatically Generating Malicious Disks using Symbolic Execution. Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar and Dawson Engler. Oakland 2006.
• Preventing memory error exploits with WIT . Periklis Akritidis, Cristian Cadar, Costin Raiciu, Manuel Costa, Miguel Castro. Oakland 2008.
• Testing for Buffer Overflows with Length Abstraction. Ru-Gang Xu and Rupak Majumdar. ISSTA 2008.

GUI Testing:

• Test Generation for Graphical User Interfaces Based on Symbolic Execution. S. Ganov, C. Killmar, S. Khurshild and D. Perry. AST 2008
• Symbolic execution for GUI testing. S. Ganov, S. Khurshid, and D. Perry. TAIC-PART 2007.

Method Sequence Generation:

• MSeqGen: object-oriented unit-test generation via mining source code, Thummalapenta, Suresh and Xie, Tao and Tillmann, Nikolai and de Halleux, Jonathan and Schulte, Wolfram, FSE 2009
• OCAT: Object Capture based Automated Testing. H. Jaygarl, S. Kim, T. Xie, and C.K. Chang ISSTA 2010

Dependency and Taint Analysis:

• Strict Control Dependence and its Effect on Dynamic Information Flow Analyses Tao Bao, Yunhui Zheng, Zhiqiang Lin, Xiangyu Zhang and Dongyan Xu ISSTA 2010

Parallel Correctness Specification:

• Koushik Sen
  • Abstract Analysis of Symbolic Executions. Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik. CAV 2010.
  • Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution. Neha Rungta, Eric G Mercer and Willem Visser. SPIN 2009.
  • Combining symbolic execution with model checking to verify parallel numerical programs. S.F. Siegel, A. Mironova, G.S. Avrunin, and L.A. Clarke. TOSEM 2008.

Others:

• An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. Kiran Lakhotia, Phil McMinn, Mark Harman. JSS 2010.
• Pex-White Box Test Generation for .NET. Nikolai Tillmann and Jonathan de Halleux. TAP 2008.
• Active property checking. Patrice Godefroid, Michael Y. Levin, and David Molnar. EMSOFT 2008.
• Predictive Testing: Amplifying the Effectiveness of Software Testing. Pallavi Joshi, Koushik Sen and Mark Shlimovich. ESEC/FSE 2007.
• Variably interprocedural program analysis for runtime error detection. Aaron Tomb, Guillame Brat, and Willem Visser. ISSTA 2007.
• JPF-SE: A Symbolic Execution Extension to Java Pathfinder. Saswat Anand, Corina Pasareanu, Willem Visser. TACAS 07
• Generalized Symbolic Execution for Model Checking and Testing, Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser, TACAS 2003.

Test Input Generation: