KLEE

master branch

Publications

Publications and Systems Using KLEE

Below you can find a list of papers and systems that either use or extend KLEE. They are listed in chronological order.

If you have used or extended KLEE and would like to have your paper listed here, please email klee-dev-owner or c.cadar@imperial.ac.uk.

  1. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
    Cristian Cadar, Daniel Dunbar, Dawson Engler
    USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008)
    December 8-10, 2008, San Diego, CA, USA

  2. Server-side Verification of Client Behavior in Online Games
    Darrell Bethea, Robert Cochran, Michael Reiter
    Network and Distributed System Security Symposium (NDSS 2010)
    February 28 - March 3, San Diego, CA, USA

  3. KleeNet: Discovering Insidious Interaction Bugs in Wireless Sensor Networks Before Deployment
    Raimondas Sasnauskas, Olaf Landsiedel, Muhammad Hamad Alizai, Carsten Weise, Stefan Kowalewski, Klaus Wehrle
    ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN 2010)
    April 12-16, 2010, Stockholm, Sweden
    KleeNet is available here.

  4. Execution Synthesis: A Technique for Automated Software Debugging
    Cristian Zamfir, George Candea
    ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2010)
    April 13-16, 2010, Paris, France

  5. Reverse Engineering of Binary Device Drivers with RevNIC
    Vitaly Chipounov, George Candea
    ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2010)
    April 13-16, 2010, Paris, France

  6. Testing Closed-Source Binary Device Drivers with DDT
    Volodymyr Kuznetsov, Vitaly Chipounov, George Candea
    USENIX Annual Technical Conference (USENIX ATC 2010)
    June 22-25, 2010, Boston, MA, USA

  7. Stable Deterministic Multithreading through Schedule Memoization
    Heming Cui, Jingyue Wu, Chia-che Tsai, Junfeng Yang
    USENIX Symposium on Operating Systems Design and Implementation (OSDI 2010)
    October 4-6, 2010, Vancouver, BC, Canada

  8. AEG: Automatic Exploit Generation
    Thanassis Avgerinos, Sang Kil Cha, Brent Lim Tze Hao, David Brumley
    Network and Distributed System Security Symposium (NDSS 2011)
    February 6-9, 2011, San Diego, CA, USA

  9. Howard: A Dynamic Excavator for Reverse Engineering Data Structures
    Asia Slowinska, Traian Stancescu, Herbert Bos
    Network and Distributed System Security Symposium (NDSS 2011)
    February 6-9, 2011, San Diego, CA, USA

  10. S2E: A Platform for In Vivo Multi-Path Analysis of Software Systems
    Vitaly Chipounov, Volodymyr Kuznetsov, George Candea
    International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011)
    March 5-11, 2011, Newport Beach, CA
    S2E is available here.

  11. Parallel Symbolic Execution for Automated Real-World Software Testing
    Stefan Bucur, Vlad Ureche, Cristian Zamfir, George Candea
    ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2011)
    April 10-13, 2011, Salzburg, Austria
    Cloud9 is available here.

  12. Symbolic Crosschecking of Floating-Point and SIMD Code
    Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
    ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2011)
    April 10-13, 2011, Salzburg, Austria

  13. Practical, Low-Effort Equivalence Verification of Real Code
    David Ramos, Dawson Engler
    Computer Aided Verification (CAV 2011)
    July 16-20, 2011, Snowbird, UT, USA

  14. Scalable Symbolic Execution of Distributed Systems
    Raimondas Sasnauskas, Oscar Soria Dustmann, Benjamin Lucien Kaminski, Carsten Weise, Stefan Kowalewski, Klaus Wehrle
    IEEE International Conference on Distributed Computing Systems (ICDCS 2011)
    June 20-24, 2011, Minneapolis, MN, USA

  15. Efficient Deterministic Multithreading through Schedule Relaxation
    Heming Cui, Jingyue Wu, John Gallagher, Huayang Guo, Junfeng Yang
    ACM Symposium on Operating Systems Principles (SOSP 2011)
    October 23-26, 2011, Cascais, Portugal

  16. KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs
    Guodong Li, Indradeep Ghosh and Sreeranga Rajan
    International Conference on Computer Aided Verification (CAV 2011)
    July 14-20, 2011, Cliff Lodge, Snowbird, UT, USA

  17. Symbolic Testing of OpenCL Code
    Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
    Haifa Verification Conference (HVC 2011)
    December 6-8, 2011, Haifa, Israel

  18. GKLEE: Concolic Verification and Test Generation for GPUs
    Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, and Sreeranga P. Rajan
    ACM Symposium on Principles and Practice of Parallel Programming (PPoPP 2012)
    February 25-29, 2012, New Orleans, LA, USA
    GKLEE is available here.

  19. Staged Symbolic Execution
    Junaid Haroon Siddiqui, Sarfraz Khurshid
    ACM Symposium on Applied Computing (SAC 2012)
    March 26-30, 2012, Trento, Italy

  20. make test-zesti: A Symbolic Execution Solution for Improving Regression Testing
    Paul Dan Marinescu, Cristian Cadar
    International Conference on Software Engineering (ICSE 2012)
    June 2-9, 2012, Zurich, Switzerland
    ZESTI is available here.

  21. BugRedux: Reproducing Field Failures for In-House Debugging
    Wei Jin, Alessandro Orso
    International Conference on Software Engineering (ICSE 2012)
    June 2-9, 2012, Zurich, Switzerland
    BugRedux is available here.

  22. Efficient State Merging in Symbolic Execution
    Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, George Candea
    Programming Language Design and Implementation (PLDI)
    June 11-16, 2012, Beijing, China

  23. Noninterference via Symbolic Execution
    Dimiter Milushev, Wim Beck, and Dave Clarke
    In: Giese H., Rosu G. (eds) Formal Techniques for Distributed Systems. Lecture Notes in Computer Science, vol 7273. Springer, Berlin, Heidelberg (FMOODS/FORTE 2012)
    June 13-16, 2012, Stockholm, Sweden

  24. High-Coverage Symbolic Patch Testing
    Paul Dan Marinescu, Cristian Cadar
    SPIN Workshop on Model Checking of Software (SPIN 2012)
    July 23-24, 2012, Oxford, UK

  25. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
    Jiri Slaby, Jan Strejcek, Marek Trtík
    Formal Methods for Industrial Critical Systems (FMICS 2012)
    August 27-28, 2012, Paris, France

  26. SymDrive: Testing Drivers without Devices
    Matthew J. Renzelmann, Asim Kadav, and Michael M. Swift
    10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2012)
    October 8-10, 2012, Hollywood, USA

  27. Scaling Symbolic Execution Using Ranged Analysis
    Junaid Haroon Siddiqui, Sarfraz Khurshid ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA 2012)
    October 19-26, 2012, Tucson, Arizona, USA

  28. Enhancing Symbolic Execution to Test the Compatibility of Re-engineered Industrial Software
    Susumu Tokumoto, Tadahiro Uehara, Kazuki Munakata, Haruyuki Ishida, Toru Eguchi, Masafumi Baba
    Asia-Pacific Software Engineering Conference
    December 4-7, 2012, Hong Kong, China

  29. Symbolic Simulation for Debugging and Analysis of REKO Models Using KLEE
    Marta Vicente Romero
    Master Thesis, Luleå University of Technology
    2013, Luleå, Sweden

  30. Automatic Detection of Floating-Point Exceptions
    Peter C. Rigby, Earl T. Barr, Christian Bird, Premkumar Devanbu, Daniel M. German
    Principles of Programming Languages (POPL)
    January 23-25, 2013, Rome, Italy

  31. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution)
    Jiri Slaby, Jan Strejcek, Marek Trtík
    International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013)
    March 16-24, 2013, Rome, Italy

  32. Post-silicon Conformance Checking with Virtual Prototypes
    Li Lei and Fei Xie and Kai Cong
    Annual Design Automation Conference (DAC 2013)
    June 1-5, 2013, San Francisco, CA, USA

  33. Redundant State Detection for Dynamic Symbolic Execution
    Suhabe Bugrara, Dawson Engler
    USENIX Annual Technical Conference (USENIX ATC 2013)
    June 26-28, 2013, San Jose, California

  34. KATCH: High-Coverage Testing of Software Patches
    Paul Dan Marinescu, Cristian Cadar
    Joint meeting of the European Software Engineering Conference and the Symposium on the Foundations of Software Engineering (ESEC/FSE 2013)
    August 18-26, 2013, St Petersburg, Russia

  35. Multi-solver Support in Symbolic Execution
    Hristina Palikareva, Cristian Cadar
    International Conference on Computer Aided Verification (CAV 2013)
    July 13-19, 2013, St Petersburg, Russia
    KLEE-Multisolver is available here.

  36. Automatic Concolic Test Generation with Virtual Prototypes for Post-silicon Validation
    Kai Cong, Fei Xie, Li Lei
    International Conference on Computer-aided Design (ICCAD 2013)
    November 18-21, 2013, San Jose, CA, USA

  37. Conflict-Driven Symbolic Execution
    Celina Gomes do Val
    Master Thesis, University of British Columbia
    March 2014, Vancouver, CA
    KITE is available here.

  38. Automated Testcase Generation for Numerical Support Functions in Embedded Systems
    Johann Schumann, and Stefan-Alexander Schneider
    6th International Symposium on NASA Formal Methods (NFM 2014)
    April 29 - May 01, 2014, Houston, TX, USA

  39. SemFix: Program Repair via Semantic Analysis
    Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury, Satish Chandra
    ACM/IEEE International Conference on Software Engineering (ICSE) 2013
    May 18-26, 2013, San Francisco, CA, USA

  40. FIE on Firmware: Finding Vulnerabilities in Embedded Systems using Symbolic Execution
    Drew Davidson, Benjamin Moench, Somesh Jha, and Thomas Ristenpart
    22nd USENIX Security Symposium (USENIX Security ‘13)
    August 14–16, 2013, Washington, D.C., USA

  41. Practical Use of Formal Verification for Safety Critical Cyber-Physical Systems: A Case Study
    Tasuku Ishigooka, Habib Saissi, Thorsten Piper, Stefan Winter and Neeraj Suri
    IEEE International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA 2014)
    August 25-26, 2014, Hong Kong, China

  42. Docovery: Toward Generic Automatic Document Recovery
    Tomasz Kuchta, Cristian Cadar, Miguel Castro, Manuel Costa
    International Conference on Automated Software Engineering (ASE) 2014
    September 15-19, 2014, Vasteras, Sweden
    Docovery is available here.

  43. Symbolic Execution of Multithreaded Programs from Arbitrary Program Contexts
    Tom Bergan, Dan Grossman, and Luis Ceze
    ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA 2014)
    October 20–24, 2014, Portland, USA

  44. Frog Program Bug Finder
    Qirong Wang, 2015
    Software testing and debugging tool combining KLEE test generation with fault localization

  45. Postconditioned Symbolic Execution
    Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, Chen Zhao
    IEEE 8th International Conference on Software Testing, Verification and Validation (ICST) 2015
    April 13-17, 2015, Graz, Austria

  46. The Use of Symbolic Execution for Testing of Real-Time Safety-Related Software
    Martin Hořeňovský
    Bachelor Thesis, Czech Technical University in Prague
    May 2015, Prague, CZ

  47. Analyzing Protocol Implementations for Interoperability
    Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, and Todd Millstein
    12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2015)
    May 4-6, 2015, Oakland, CA, USA
    PIC is available here.

  48. DASE: Document-Assisted Symbolic Execution for Improving Automated Software Testing
    Edmund Wong, Lei Zhang, Song Wang, Taiyue Liu, and Lin Tan
    International Conference on Software Engineering (ICSE 2015)
    May 16-24, 2015, Florence, Italy

  49. A Framework for Measuring Software Obfuscation Resilience Against Automated Attacks
    Sebastian Banescu, Martin Ochoa, Alexander Pretschner
    International Workshop on Software Protection (SPRO 2015)
    May 17, 2015, Florence, Italy

  50. Parallel SMT Solving and Concurrent Symbolic Execution
    Emil Rakadjiev, Taku Shimosawa, Hiroshi Mine, Satoshi Oshima
    IEEE Trustcom/BigDataSE/ISPA 2015
    August 20-22, 2015, Helsinki, Finland

  51. Parallel Symbolic Execution: Merging In-Flight Requests
    Martin Nowack, Katja Tietze, and Christof Fetzer
    11th Haifa Verification Conference (HVC 2015)
    November 17-19, 2015, Haifa, Israel

  52. Studying the Influence of Standard Compiler Optimizations on Symbolic Execution
    Shiyu Dong, Oswaldo Olivo, Lingming Zhang, Sarfraz Khurshid
    IEEE International Symposium on Software Reliability Engineering (ISSRE 2015)
    November 2-5, 2015, Gaithersbury, MD, USA

  53. Generating High Coverage Tests for SystemC Designs Using Symbolic Execution
    Bin Lin, Zhenkun Yang, Kai Cong, and Fei Xie
    21st Asia and South Pacific Design Automation Conference (ASP-DAC 2016)
    January 25-28, 2016, Macau, China

  54. Profiting from Unit Tests for Integration Testing
    Dominik Holling, Andreas Hofbauer, Alexander Pretschner, Matthias Gemmar
    IEEE 9th International Conference on Software Testing, Verification and Validation (ICST) 2016
    April 11-15, 2016, Chicago, IL, USA

  55. Nequivack: Assessing Mutation Score Confidence
    Dominik Holling, Sebastian Banescu, Marco Probst, Ana Petrovska, Alexander Pretschner
    IEEE 9th International Conference on Software Testing, Verification and Validation (ICST) 2016
    April 11-15, 2016, Chicago, IL, USA

  56. Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis
    Sergey Mechtaev, Jooyong Yi, Abhik Roychoudhury
    ACM/IEEE International Conference on Software Engineering (ICSE) 2016
    May 14-22, 2016, Austin, Texas, USA
    Angelix is available here.

  57. Shadow of a Doubt: Testing for Divergences Between Software Versions
    Hristina Palikareva, Tomasz Kuchta, Cristian Cadar
    International Conference on Software Engineering (ICSE) 2016
    May 14-22, 2016, Austin, Texas, USA
    Shadow is available here.

  58. On the Techniques We Create, the Tools We Build, and Their Misalignments: A Study of KLEE
    Eric F. Rizzi, Sebastian Elbaum, Matthew B. Dwyer
    International Conference on Software Engineering (ICSE) 2016
    May 14-22, 2016, Austin, Texas, USA

  59. Automatic Generation of High-coverage Tests for RTL Designs Using Software Techniques and Tools
    Yu Zhang, Wenlong Feng, Mengxing Huang
    IEEE Conference on Industrial Electronics and Applications (ICIEA) 2016
    June 5-7, 2016, Hefei, China

  60. MACKE: Compositional Analysis of Low-level Vulnerabilities with Symbolic Execution
    Saahil Ognawala, Martín Ochoa, Alexander Pretschner, Tobias Limmer
    IEEE/ACM International conference on Automated Software Engineering (ASE 2016)
    September 3-7, 2016, Singapore, Singapore

  61. Building Robust Distributed Systems and Network Protocols by Using Adversarial Testing and Behavioral Analysis
    Endadul Hoque, Cristina Nita-Rotaru
    IEEE Cybersecurity Development (SecDev) 2016
    November 3-4, 2016, Boston, MA, USA

  62. Hotspot Symbolic Execution of Floating-point Programs
    Minghui Quan
    24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016)
    November 13-18, 2016, Seattle, WA, USA

  63. Eliminating Path Redundancy via Postconditioned Symbolic Execution
    Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, and Chen Zhao
    IEEE Transactions on Software Engineering, Volume: PP, Issue: 99
    January 26, 2017

  64. Patch-related Vulnerability Detection Based on Symbolic Execution
    Weizhong Qiang, Yuehua Liao, Guozhong Sun, Laurence T. Yang, Deqing Zou, and Hai Jin
    IEEE Access, vol. PP, no. 99
    March 1, 2017

  65. Case Study on LLVM as Suitable Intermediate Language for Binary Analysis
    Florian Märkl
    Seminar “Reverse Code Engineering” Winter 2016/2017, Technische Universität München
    March 22, 2017, Munich, Germany

  66. Non-Semantics-Preserving Transformations for Higher-Coverage Test Generation Using Symbolic Execution
    Hayes Converse, Oswaldo Olivo, Sarfraz Khurshid
    IEEE 10th International Conference on Software Testing, Verification and Validation (ICST) 2017
    March 13-17, 2017, Tokyo, Japan

  67. Heuristically Matching Solution Spaces of Arithmetic Formulas to Efficiently Reuse Solutions
    Andrea Aquino, Giovanni Denaro, and Mauro Pezzè
    ACM/IEEE International Conference on Software Engineering (ICSE) 2017
    May 20-28, 2017, Buenos Aires, Argentina

  68. An Empirical Study on Mutation, Statement and Branch Coverage Fault Revelation that Avoids the Unreliable Clean Program Assumption
    Thierry Titcheu Chekam, Mike Papadakis, Yves Le Traon, and Mark Harman
    ACM/IEEE International Conference on Software Engineering (ICSE) 2017
    May 20-28, 2017, Buenos Aires, Argentina

  69. pbSE: Phase-Based Symbolic Execution
    Qixue Xiao, Yu Chen, Chengang Wu, Kang Li, and Junjie Mao
    47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2017)
    June 26-19, 2017, Denver, CO, USA

  70. Accelerating Array Constraints in Symbolic Execution
    David M. Perry, Andrea Mattavelli, Xiangyu Zhang, Cristian Cadar
    International Symposium on Software Testing and Analysis (ISSTA 2017)
    July 10-14, 2017, Santa Barbara, CA, USA
    KLEE-Array is available here.

  71. Failure-Directed Program Trimming
    Kostas Ferles, Valentin Wüstholz, Maria Christakis, and Isil Dillig
    11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2017)
    September 4-8, 2017, Paderborn, Germany

  72. Symbolic Execution of Programmable Logic Controller Code
    Shengjian Guo, Meng Wu, and Chao Wang
    11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2017)
    September 4-8, 2017, Paderborn, Germany

  73. Did we Learn from LLC Side Channel Attacks? A Cache Leakage Detection Tool for Crypto Libraries
    Gorka Irazoqui, Kai Cong, Xiaofei Guo, Hareesh Khattri, Arun Kanuparthi, Thomas Eisenbarth, and Berk Sunar
    arXiv, September 5, 2017

  74. KLOVER: Automatic Test Generation for C and C++ Programs, Using Symbolic Execution
    Guodong Li, Takuki Kamiya, Indradeep Ghosh, Sreeranga Rajan, Susumu Tokumoto, Kazuki Munakata, and Tadahiro Uehara
    IEEE Software (Volume: 34, Issue: 5, 2017)
    September 22, 2017

  75. Effectiveness of Synthesis in Concolic Deobfuscation
    Fabrizio Biondi, Sébastien Josse, Axel Legay, Thomas Sirvent
    Computers & Security (Volume: 70, 2017)
    September 2017

  76. Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing
    Timotej Kapus, Cristian Cadar
    IEEE/ACM International conference on Automated Software Engineering (ASE 2017)
    October 30 - November 3, 2017, Urbana-Champaign, IL, USA

  77. Floating-Point Symbolic Execution: A Case Study in N-version Programming
    Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair Donaldson, Rafael Zähl, Klaus Wehrle
    IEEE/ACM International conference on Automated Software Engineering (ASE 2017)
    October 30 - November 3, 2017, Urbana-Champaign, IL, USA