| | | | |
|---|
| 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 |
| 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 |
| 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 | |
| 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 | |
| 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 | |