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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  39. 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, 2015, Austin, Texas, USA
    Shadow is available here.