Publications
Publications and Systems Using KLEE
Below you can find a list of 100+ papers and systems that either use or extend KLEE. They are listed in chronological order.
Additional information about systems and research based on KLEE can be found on the website of the 1st International KLEE Workshop on Symbolic Execution.
If you have used or extended KLEE and would like to have your paper listed here, please open a pull request at https://github.com/klee/klee.github.io/pulls. Alternatively, email klee-dev-owner or c.cadar@imperial.ac.uk.
-
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 -
HAMPI: A Solver for String Constraints
Adam Kiezun, Vijay Ganesh, Philip Guo, Pieter Hooimeijer, Michael Ernst
International Symposium on Software Testing and Analysis (ISSTA 2009)
July 19-23, 2009, Chicago, IL, USA -
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, 2010, San Diego, CA, USA -
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. -
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 -
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 -
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 -
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 -
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 -
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 -
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 at EPFL and GitHub. -
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. -
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 -
Scalable Symbolic Execution of Distributed Systems
Raimondas Sasnauskas, Oscar 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 -
KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs
Guodong Li, Indradeep Ghosh, Sreeranga Rajan
International Conference on Computer Aided Verification (CAV 2011)
July 14-20, 2011, Cliff Lodge, Snowbird, UT, USA -
Practical, Low-Effort Equivalence Verification of Real Code
David Ramos, Dawson Engler
International Conference on Computer Aided Verification (CAV 2011)
July 16-20, 2011, Snowbird, UT, USA -
Selecting Peers for Execution Comparison
William N. Sumner, Tao Bao, Xiangyu Zhang
ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2011)
July 17-21, 2011, Toronto, CA -
Directed Symbolic Execution
Kin-Keung Ma, Khoo Yit Phang, Jeffrey S. Foster, Michael Hicks
International Conference on Static Analysis (SAS 2011)
September 14-16, 2011, Venice, Italy -
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 -
Symbolic Testing of OpenCL Code
Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
Haifa Verification Conference (HVC 2011)
December 6-8, 2011, Haifa, Israel -
GKLEE: Concolic Verification and Test Generation for GPUs
Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, 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. -
Staged Symbolic Execution
Junaid Haroon Siddiqui, Sarfraz Khurshid
ACM Symposium on Applied Computing (SAC 2012)
March 26-30, 2012, Trento, Italy -
Scalable Testing of File System Checkers
João Carlos Menezes Carreira, Rodrigo Rodrigues, George Candea, Rupak Majumdar
ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys 2012)
April 10-13, 2012, Bern, Switzerland -
make test-zesti: A Symbolic Execution Solution for Improving Regression Testing
Paul Dan Marinescu, Cristian Cadar
ACM/IEEE International Conference on Software Engineering (ICSE 2012)
June 2-9, 2012, Zurich, Switzerland
ZESTI is available here. -
BugRedux: Reproducing Field Failures for In-House Debugging
Wei Jin, Alessandro Orso
ACM/IEEE International Conference on Software Engineering (ICSE 2012)
June 2-9, 2012, Zurich, Switzerland
BugRedux is available here. -
Industrial Application of Concolic Testing Approach: A Case Study on libexif by Using CREST-BV and KLEE
Yunho Kim, Moonzoo Kim, YoungJoo Kim, Yoonkyu Jang
ACM/IEEE International Conference on Software Engineering (ICSE 2012)
June 2-9, 2012, Zurich, Switzerland -
Efficient State Merging in Symbolic Execution
Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, George Candea
ACM Conference on Programming Language Design and Implementation (PLDI 2012)
June 11-16, 2012, Beijing, China -
Noninterference via Symbolic Execution
Dimiter Milushev, Wim Beck, 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 -
CRAX: Software Crash Analysis for Automatic Exploit Generation by Modeling Attacks as Symbolic Continuations
Shih-Kun Huang, Min-Hsiang Huang, Po-Yen Huang, Chung-Wei Lai, Han-Lin Lu, Wai-Meng Leong
International Conference on Software Security and Reliability (SERE 2012)
June 20-22, 2012, Gaithersburg, USA -
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 -
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
Jiri Slaby, Jan Strejcek, Marek Trtík
International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2012)
August 27-28, 2012, Paris, France -
SymDrive: Testing Drivers without Devices
Matthew J. Renzelmann, Asim Kadav, Michael M. Swift
USENIX Symposium on Operating Systems Design and Implementation (OSDI 2012)
October 8-10, 2012, Hollywood, USA -
Scaling Symbolic Execution Using Ranged Analysis
Junaid Haroon Siddiqui, Sarfraz Khurshid
ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012)
October 19-26, 2012, Tucson, Arizona, USA -
Detecting Problematic Message Sequences and Frequencies in Distributed Systems
Charles Lucas, Sebastian Elbaum, David S. Rosenblum
ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012)
October 19-26, 2012, Tucson, USA -
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 -
A SOFT Way for OpenFlow Switch Interoperability Testing
Maciej Kuzniar, Peter Peresini, Marco Canini, Daniele Venzano, Dejan Kostic
International Conference on emerging Networking EXperiments and Technologies (CoNEXT 2012)
December 10-13, 2012, Nice, France -
Symbolic Simulation for Debugging and Analysis of REKO Models Using KLEE
Marta Vicente Romero
Master Thesis, Luleå University of Technology
2013, Luleå, Sweden -
Automatic Detection of Floating-Point Exceptions
Peter C. Rigby, Earl T. Barr, Christian Bird, Premkumar Devanbu, Daniel M. German
ACM Symposium on Principles of Programming Languages (POPL 2013)
January 23-25, 2013, Rome, Italy -
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
Symbiotic is available here. -
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 -
Post-silicon Conformance Checking with Virtual Prototypes
Li Lei, Fei Xie, Kai Cong
Design Automation Conference (DAC 2013)
June 1-5, 2013, San Francisco, CA, USA -
CLAP: Recording Local Executions to Reproduce Concurrency Failures
Jeff Huang, Charles Zhang, Julian Dolby
ACM Conference on Programming Language Design and Implementation (PLDI 2013)
June 16-22, 2013, Seattle, WA, USA -
CRAXweb: Automatic Web Application Testing and Attack Generation
Shih-Kun Huang, Han-Lin Lu, Wai-Meng Leong, Huan Liu
International Conference on Software Security and Reliability (SERE 2013)
June 18-20, 2013, Gaithersburg, USA -
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 -
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. -
F3: Fault Localization for Field Failures
Wei Jin, Alessandro Orso
International Symposium on Software Testing and Analysis (ISSTA 2013)
July 15-20, 2013, Lugano, Switzerland -
FIE on Firmware: Finding Vulnerabilities in Embedded Systems using Symbolic Execution
Drew Davidson, Benjamin Moench, Somesh Jha, Thomas Ristenpart
22nd USENIX Security Symposium (USENIX Security ‘13)
August 14–16, 2013, Washington, D.C., USA -
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 -
Symbolic Software Model Validation
Cynthia Sturton, Rohit Sinha, Thurston H.Y. Dang, Sakshi Jain, Michael McCoyd, Wei Yang Tan, Petros Maniatis, Sanjit A. Seshia, David Wagner
ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCON 2013)
October 18-20, 2013, Portland, USA -
Steering Symbolic Execution to Less Traveled Paths
You Li, Zhendong Su, Linzhang Wang, Xuandong Li
ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA 2013)
October 26-31, 2013, Indianapolis, USA -
Modeling Firmware as Service Functions and Its Application to Test Generation
Sunha Ahn, Sharad Malik
Haifa Verification Conference (HVC 2013)
November 5-7, 2013, Haifa, Israel -
Chaining Test Cases for Reactive System Testing
Peter Schrammel, Tom Melham, Daniel Kroening
IFIP International Conference on Testing Software and Systems (ICTSS 2013)
November 13-15, 2013, Istanbul, Turkey -
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 -
Static Analysis Driven Cache Performance Testing
Abhijeet Banerjee, Sudipta Chattopadhyay, Abhik Roychoudhury
IEEE Real-Time Systems Symposium (RTSS 2013)
December 3-6, 2013, Vancouver, CA -
Conflict-Driven Symbolic Execution
Celina Gomes do Val
Master Thesis, University of British Columbia
March 2014, Vancouver, CA
KITE is available here. -
Reproducing Field Failures for Programs with Complex Grammar-Based Input
Fitsum Meshesha Kifetew, Wei Jin, Roberto Tiella, Alessandro Orso, Paolo Tonella
IEEE International Conference on Software Testing, Verification and Validation (ICST 2014)
March 31 - April 4, 2014, Cleveland, USA -
Automated Testcase Generation for Numerical Support Functions in Embedded Systems
Johann Schumann, Stefan-Alexander Schneider
International Symposium on NASA Formal Methods (NFM 2014)
April 29 - May 1, 2014, Houston, TX, USA -
Practical Use of Formal Verification for Safety Critical Cyber-Physical Systems: A Case Study
Tasuku Ishigooka, Habib Saissi, Thorsten Piper, Stefan Winter, Neeraj Suri
IEEE International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA 2014)
August 25-26, 2014, Hong Kong, China -
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. -
Control Flow Obfuscation using Neural Network to Fight Concolic Testing
Haoyu Ma, Xinjie Ma, Weijie Liu, Zhipeng Huang, Debin GAO, Chunfu Jia
International Conference on Security and Privacy in Communication Networks (SecureComm 2014)
September 24-26, 2014, Beijing, China -
Automated Software Testing of Memory Performance in Embedded GPUs
Sudipta Chattopadhyay, Petru Eles, Zebo Peng
International Conference on Embedded Software (EMSOFT 2014)
October 12-17, 2014, Jaypee Greens, India -
Symbolic Execution of Multithreaded Programs from Arbitrary Program Contexts
Tom Bergan, Dan Grossman, Luis Ceze
ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2014)
October 20-24, 2014, Portland, USA -
Methods for Binary Symbolic Execution
Anthony Romano
Dissertation, Stanford University, Department of Computer Science
December 2014, Stanford, USA -
Frog Program Bug Finder
Qirong Wang, 2015
Software testing and debugging tool combining KLEE test generation with fault localization -
Postconditioned Symbolic Execution
Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, Chen Zhao
IEEE International Conference on Software Testing, Verification and Validation (ICST 2015)
April 13-17, 2015, Graz, Austria -
Generating Succinct Test Cases Using Don’t Care Analysis
Cuong Nguyen, Hiroaki Yoshida, Mukul Prasad, Indradeep Ghosh, Koushik Sen
IEEE International Conference on Software Testing, Verification and Validation (ICST 2015)
April 13-17, 2015, Graz, Austria -
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 -
Analyzing Protocol Implementations for Interoperability
Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, Todd Millstein
USENIX Symposium on Networked Systems Design and Implementation (NSDI 2015)
May 4-6, 2015, Oakland, CA, USA
PIC is available here. -
A Synergistic Analysis Method for Explaining Failed Regression Tests
Qiuping Yi, Zijiang Yang, Jian Liu, Chen Zhao, Chao Wang
ACM/IEEE International Conference on Software Engineering (ICSE 2015)
May 16-24, 2015, Florence, Italy -
DASE: Document-Assisted Symbolic Execution for Improving Automated Software Testing
Edmund Wong, Lei Zhang, Song Wang, Taiyue Liu, Lin Tan
International Conference on Software Engineering (ICSE 2015)
May 16-24, 2015, Florence, Italy -
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 -
Explaining Software Failures by Cascade Fault Localization
Qiuping Yi, Zijiang Yang, Jian Liu, Chen Zhao, Chao Wang
ACM Transactions on Design Automation of Electronic Systems, Volume 20 Issue 3 (TODAES)
June, 2015 -
Symbolic Execution for BIOS Security
Oleksandr Bazhaniuk, John Loucaides, Lee Rosenbaum, Mark R. Tuttle, Vincent Zimmer
USENIX Workshop on Offensive Technologies (WOOT 2015)
August 10-11, 2015, Washington D.C., USA -
Under-Constrained Symbolic Execution: Correctness Checking for Real Code
David A. Ramos, Dawson Engler
USENIX Security Symposium (SEC 2015)
August 12-14, 2015, Washington D.C., USA -
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 -
Parallel Symbolic Execution: Merging In-Flight Requests
Martin Nowack, Katja Tietze, Christof Fetzer
Haifa Verification Conference (HVC 2015)
November 17-19, 2015, Haifa, Israel -
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 -
Generating High Coverage Tests for SystemC Designs Using Symbolic Execution
Bin Lin, Zhenkun Yang, Kai Cong, Fei Xie
Asia and South Pacific Design Automation Conference (ASP-DAC 2016)
January 25-28, 2016, Macau, China -
Profiting from Unit Tests for Integration Testing
Dominik Holling, Andreas Hofbauer, Alexander Pretschner, Matthias Gemmar
IEEE International Conference on Software Testing, Verification and Validation (ICST 2016)
April 11-15, 2016, Chicago, IL, USA -
Nequivack: Assessing Mutation Score Confidence
Dominik Holling, Sebastian Banescu, Marco Probst, Ana Petrovska, Alexander Pretschner
IEEE International Conference on Software Testing, Verification and Validation (ICST 2016)
April 11-15, 2016, Chicago, IL, USA -
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. -
Shadow of a Doubt: Testing for Divergences Between Software Versions
Hristina Palikareva, Tomasz Kuchta, Cristian Cadar
ACM/IEEE International Conference on Software Engineering (ICSE 2016)
May 14-22, 2016, Austin, Texas, USA
Shadow is available here. -
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 -
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 -
Automated Feedback Framework for Introductory Programming Courses
Jianxiong Gao, Bei Pang, Steven S. Lumetta
Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2016)
July 11-13, 2016, Arequipa, Peru -
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 -
LLSPLAT: Improving Concolic Testing by Bounded Model Checking
Min Gao, Lei He, Rupak Majumdar, Zilong Wang
IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016)
October 2-3, 2016, Raleigh, NC, USA -
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 -
Hotspot Symbolic Execution of Floating-point Programs
Minghui Quan
ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016)
November 13-18, 2016, Seattle, WA, USA -
Eliminating Path Redundancy via Postconditioned Symbolic Execution
Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, Chen Zhao
IEEE Transactions on Software Engineering, Volume: PP, Issue: 99
January 26, 2017 -
Patch-related Vulnerability Detection Based on Symbolic Execution
Weizhong Qiang, Yuehua Liao, Guozhong Sun, Laurence T. Yang, Deqing Zou, Hai Jin
IEEE Access, vol. PP, no. 99
March 1, 2017 -
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 -
Non-Semantics-Preserving Transformations for Higher-Coverage Test Generation Using Symbolic Execution
Hayes Converse, Oswaldo Olivo, Sarfraz Khurshid
IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
March 13-17, 2017, Tokyo, Japan -
Heuristically Matching Solution Spaces of Arithmetic Formulas to Efficiently Reuse Solutions
Andrea Aquino, Giovanni Denaro, Mauro Pezzè
ACM/IEEE International Conference on Software Engineering (ICSE 2017)
May 20-28, 2017, Buenos Aires, Argentina -
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, Mark Harman
ACM/IEEE International Conference on Software Engineering (ICSE 2017)
May 20-28, 2017, Buenos Aires, Argentina -
SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations
Sze Yiu Chau, Omar Chowdhury, Endadul Hoque, Huangyi Ge, Aniket Kate, Cristina Nita-Rotaru, Ninghui Li
IEEE Symposium on Security and Privacy (S&P 2017)
May 22-24, 2017, San Jose, CA, USA -
Analyzing Operational Behavior of Stateful Protocol Implementations for Detecting Semantic Bugs
Endadul Hoque, Omar Chowdhury, Sze Yiu Chau, Cristina Nita-Rotaru, Ninghui Li
IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2017)
June 26-29, 2017, Denver, CO, USA -
pbSE: Phase-Based Symbolic Execution
Qixue Xiao, Yu Chen, Chengang Wu, Kang Li, Junjie Mao
IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2017)
June 26-29, 2017, Denver, CO, USA -
StatSym: Vulnerable Path Discovery through Statistics-Guided Symbolic Execution
Fan Yao, Yongbo Li, Yurong Chen
IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2017)
June 26-29, 2017, Denver, USA -
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. -
Automatic Detection and Validation of Race Conditions in Interrupt-Driven Embedded Software
Yu Wang, Linzhang Wang, Tingting Yu, Jianhua Zhao, Xuandong Li
International Symposium on Software Testing and Analysis (ISSTA 2017)
July 10-14, 2017, Santa Barbara, CA, USA -
Effectiveness of Synthesis in Concolic Deobfuscation
Fabrizio Biondi, Sébastien Josse, Axel Legay, Thomas Sirvent
Computers & Security (Volume: 70, 2017)
September 2017 -
Failure-Directed Program Trimming
Kostas Ferles, Valentin Wüstholz, Maria Christakis, Isil Dillig
Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2017)
September 4-8, 2017, Paderborn, Germany -
Symbolic Execution of Programmable Logic Controller Code
Shengjian Guo, Meng Wu, Chao Wang
Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2017)
September 4-8, 2017, Paderborn, Germany -
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, Berk Sunar
arXiv, September 5, 2017 -
KLOVER: Automatic Test Generation for C and C++ Programs, Using Symbolic Execution
Guodong Li, Takuki Kamiya, Indradeep Ghosh, Sreeranga Rajan, Susumu Tokumoto, Kazuki Munakata, Tadahiro Uehara
IEEE Software (Volume: 34, Issue: 5, 2017)
September 22, 2017 -
Quantifying the Information Leak in Cache Attacks via Symbolic Execution
Sudipta Chattopadhyay, Moritz Beck, Ahmed Rezine, Andreas Zeller
ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017)
September 29 - October 2, 2017, Vienna, Austria -
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 -
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 -
New Directions for Container Debloating
Vaibhav Rastogi, Chaitra Niddodi, Sibin Mohan, Somesh Jha
Workshop on Forming an Ecosystem Around Software Transformation (FEAST 2017)
November 3, 2017, Dallas, USA -
Souper: A Synthesizing Superoptimizer
Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, John Regehr
arXiv, November 13, 2017
Souper is available here. -
Resilience Evaluation via Symbolic Fault Injection on Intermediate Code
Hoang M. Le, Vladimir Herdt, Daniel Große, Rolf Drechsler
Design, Automation and Test in Europe (DATE 2018)
March 19 - 23, 2018, Dresden, Germany -
Symbolic Assertion Mining for Security Validation
Alessandro Danese, Valeria Bertacco, Graziano Pravadelli
Design, Automation & Test in Europe (DATE 2018)
March 19 - 23, 2018, Dresden, Germany -
Uncovering Bugs in P4 Programs with Assertion-based Verification
Lucas Freire, Miguel Neves, Lucas Leal, Kirill Levchenko, Alberto Schaeffer-Filho, Marinho Barcellos
Symposium on SDN Research (SOSR 2018)
March 28-29, 2018, Los Angeles, USA -
CRETE: A Versatile Binary-Level Concolic Testing Framework
Bo Chen, Christopher Havlicek, Zhenkun Yang, Kai Cong, Raghudeep Kannavara, Fei Xie
International Conference on Fundamental Approaches to Software Engineering (FASE 2018)
April 14-20, 2018, Thessaloniki, Greece
CRETE is available here. -
Map2Check Using LLVM and KLEE
Rafael Menezes, Herbert Rocha, Lucas Cordeiro, Raimundo Barreto
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)
April 14-20, 2018, Thessaloniki, Greece
Map2Check is available here. -
Evaluating Manual Intervention to Address the Challenges of Bug Finding with KLEE
John Galea, Sean Heelan, Daniel Neville, Daniel Kroening
arXiv, May 9, 2018 -
Chopped Symbolic Execution
David Trabish, Andrea Mattavelli, Noam Rinetzky, Cristian Cadar
ACM/IEEE International Conference on Software Engineering (ICSE 2018)
May 27 - June 3, 2018, Gothenburg, Sweden
Chopper is available here. -
SAFL: Increasing and Accelerating Testing Coverage with Symbolic Execution and Guided Fuzzing
Mingzhe Wang, Jie Liang, Yuanliang Chen, Yu Jiang, Xun Jiao, Han Liu, Xibin Zhao, Jiaguang Sun
ACM/IEEE International Conference on Software Engineering (ICSE 2018 Companion)
May 27 - June 3, 2018, Gothenburg, Sweden
(Demo on Youtube) -
Semantic Program Repair Using a Reference Implementation
Sergey Mechtaev, Manh-Dung Nguyen, Yannic Noller, Lars Grunske, Abhik Roychoudhury
ACM/IEEE International Conference on Software Engineering (ICSE 2018)
May 27 - June 3, 2018, Gothenburg, Sweden -
Indexing Operators to Extend the Reach of Symbolic Execution
Earl T. Barr, David Clark, Mark Harman, Alexandru Marginean
arXiv, June 26, 2018 -
Symbolic Liveness Analysis for Real-World Software
Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle
International Conference on Computer Aided Verification (CAV 2018)
July 14-17, 2018, Oxford, UK
Implementation is available here. -
Learning to Accelerate Symbolic Execution via Code Transformation
Junjie Chen, Wenxiang Hu, Lingming Zhang, Dan Hao, Sarfraz Khurshid, Lu Zhang
European Conference on Object-Oriented Programming (ECOOP 2018)
July 15-21, 2018, Amsterdam, Netherlands -
No Panic! Verification of Rust Programs by Symbolic Execution
Marcus Lindner, Jorge Aparicius, Per Lindgren
IEEE International Conference on Industrial Informatics (INDIN 2018)
July 18-20, 2018, Porto, Protugal
cargo-klee is available here. -
Symbolic Execution of Security Protocol Implementations: Handling Cryptographic Primitives
Mathy Vanhoef, Frank Piessens
USENIX Workshop on Offensive Technologies (WOOT 2018)
August 13-14, 2018, Baltimore, USA -
Inception: System-Wide Security Testing of Real-World Embedded Systems Software
Nassim Corteggiani, Giovanni Camurati, Aurélien Francillon
USENIX Security Symposium (Security 2018)
August 15-17, 2018, Baltimore, USA
Inception is available here. -
CPA-SymExec: Efficient Symbolic Execution in CPAchecker
Dirk Beyer, Thomas Lemberger
International Conference on Automated Software Engineering (ASE 2018)
September 3-7, 2018, Montpellier, France -
Loop Path Reduction by State Pruning
Jianxiong Gao, Steven S. Lumetta
International Conference on Automated Software Engineering (ASE 2018)
September 3-7, 2018, Montpellier, France -
PARTI: A Multi-interval Theory Solver for Symbolic Execution
Oscar Soria Dustmann, Klaus Wehrle, Cristian Cadar
International Conference on Automated Software Engineering (ASE 2018)
September 3-7, 2018, Montpellier, France -
End-to-End Automated Exploit Generation for Validating the Security of Processor Designs
Rui Zhang, Calvin Deutschbein, Peng Huang, Cynthia Sturton
IEEE/ACM International Symposium on Microarchitecture (MICRO 2018)
October 20-24, 2018, Fukuoka, Japan
Coppelia is available here. -
Automata Learning for Symbolic Execution
Bernhard K. Aichernig, Roderick Bloem, Masoud Ebrahimi, Martin Tappler, Johannes Winter
Formal Methods in Computer Aided Design (FMCAD 2018)
October 30 - November 2, 2018, Austin, USA -
Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing Leaks
Shengjian Guo, Meng Wu, Chao Wang
Joint meeting of the European Software Engineering Conference and the Symposium on the Foundations of Software Engineering (ESEC/FSE 2018)
November 4-9, 2018, Lake Buena Vista, USA -
Symbolic Execution with Existential Second-Order Constraints
Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury
Joint meeting of the European Software Engineering Conference and the Symposium on the Foundations of Software Engineering (ESEC/FSE 2018)
November 4-9, 2018, Lake Buena Vista, USA -
Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution
Felix Rath, Daniel Schemmel, Klaus Wehrle
Workshop on the Evolution, Performance, and Interoperability of QUIC (EPIQ 2018)
December 4, 2018, Heraklion, Greece -
Boost Symbolic Execution Using Dynamic State Merging and Forking
Chao Zhang Weiliang Yin Zhiqiang Lin
International Workshop on Quantitative Approaches to Software Quality (QuASoQ 2018)
December 4, 2018, Nara, Japan -
Quantifying the Information Leakage in Cache Attacks via Symbolic Execution
Moritz Beck, Ahmed Rezine, Andreas Zeller
ACM Transactions on Embedded Computing Systems, Volume 18, Issue: 1 (TECS)
February, 2019 -
Analyzing Semantic Correctness with Symbolic Execution: A Case Study on PKCS#1 v1.5 Signature Verification
Sze Yiu Chau, Moosa Yahyazadeh, Omar Chowdhury, Aniket Kate, Ninghui Li
Network and Distributed System Security Symposium (NDSS 2019)
February 24-27, 2019, San Diego, USA -
Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints
Shen Shiqi, Shweta Shinde, Soundarya Ramesh, Abhik Roychoudhury, Prateek Saxena
Network and Distributed System Security Symposium (NDSS 2019)
February 24-27, 2019, San Diego, USA -
Compositional Fuzzing Aided by Targeted Symbolic Execution
Saahil Ognawala, Fabian Kilger, Alexander Pretschner
arXiv, March 7, 2019 -
Symbolic Execution based Verification of Compliance with the ISO 26262 Functional Safety Standard
Mazen Ahmed, Mona Safar
International Conference on Design and Technology of Integrated Systems in Nanoscale Era (DTIS 2019)
April 16-18, 2019, Mykonos, Greece -
Mimicking User Behavior to Improve In-House Test Suites
Qianqian Wang, Alessandro Orso
IEEE/ACM International Conference on Software Engineering (ICSE 2019)
May 25-31, 2019, Montreal, Canada -
Zero-Overhead Path Prediction with Progressive Symbolic Execution
Richard Rutledge, Sunjae Park, Haider Khan, Alessandro Orso, Milos Prvulovic, Alenka Zajic
IEEE/ACM International Conference on Software Engineering (ICSE 2019)
May 25-31, 2019, Montreal, Canada
pg-klee is available here. -
ApproxSymate: Path Sensitive Program Approximation using Symbolic Execution
Himeshi De Silva, Andrew E. Santosa, Nhut-Minh Ho, Weng-Fai Wong
ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2019)
June 23, 2019, Phoenix, USA
ApproxSymate is available here. -
Computing Summaries of String Loops in C for Better Testing and Refactoring
Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Cristian Cadar
ACM Conference on Programming Language Design and Implementation (PLDI 2019)
June 24-26, 2019, Phoenix, USA -
Deferred Concretization in Symbolic Execution via Fuzzing
Awanish Pandey, Phani Raj Goutham Kotcharlakota, Subhajit Roy
ACM International Symposium on Software Testing and Analysis (ISSTA 2019)
July 15-19, 2019, Beijing, China -
Verification of Safety Functions Implemented in Rust - a Symbolic Execution based approach
Marcus Lindner, Nils Fitinghoff, Johan Eriksson, Per Lindgren
IEEE International Conference on Industrial Informatics (INDIN 2019)
July 22-25, Helsinki, Finland -
SCSE: Boosting Symbolic Execution via State Concretization
Huibin Wang, Chunqiang Li, Jianyi Meng, Xiaoyan Xiang
IEICE Transactions on Information and Systems (Issue 8)
August 2019 -
A Segmented Memory Model for Symbolic Execution
Timotej Kapus, Cristian Cadar
ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2019)
August 26-30, 2019, Tallin, Estonia
The implementation is available here. -
Target-Driven Compositional Concolic Testing with Function Summary Refinement for Effective Bug Detection
Yunho Kim, Shin Hong, Moonzoo Kim
ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2019)
August 26-30, 2019, Tallin, Estonia -
KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution
Guanhua Wang, Sudipta Chattopadhyay, Arnab Kumar Biswas, Tulika Mitra, Abhik Roychoudhury
arXiv, September 2, 2019
KLEESpectre is available here. -
Constraints in Dynamic Symbolic Execution: Bitvectors or Integers?
Timotej Kapus, Martin Nowack, Cristian Cadar
International Conference on Tests and Proofs (TAP 2019)
October 9-11, 2019, Porto, Portugal -
SpecuSym: Speculative Symbolic Execution for Cache Timing Leak Detection
Shengjian Guo, Yueqi Chen, Peng Li, Yueqiang Cheng, Huibo Wang, Meng Wu, Zhiqiang Zuo
arXiv, November 4, 2019 -
Fine-grain Memory Object Representation in Symbolic Execution
Martin Nowack
International Conference on Automated Software Engineering (ASE 2019)
November 10-15, 2019, San Diego, USA -
SAVIOR: Towards Bug-Driven Hybrid Testing
Yaohui Chen, Peng Li, Jun Xu, Shengjian Guo, Rundong Zhou, Yulong Zhang, Taowei, Long Lu
IEEE Symposium on Security and Privacy (S&P 2020)
May 18-20, 2020, San Francisco, USA
SAVIOR is available here. -
MEUZZ: Smart Seed Scheduling for Hybrid Fuzzing
Yaohui Chen, Mansour Ahmadi, Reza Mirzazade farkhani, Boyu Wang, Long Lu
arXiv, February 20, 2020