KLEE Workshop 2021

Since the organizers are in Europe and our speakers span three different continents – Asia, Europe and North America – we have decided to have one day (10 June) be Europe/North America friendly, and the other one (11 June) be Asia/Europe friendly. The keynote is placed so that it starts at 8am for our speaker and between 8am and midnight across the timezones of our presenters.

Regular presentations will be 12 minutes long, followed by 3 minutes of Q&A. Each session will have a discussion at the end with all the presenters in that session, where more questions can be asked.

All times are using British Summer Time (GMT+1).

Day One: 10 June 2021

15:40 – 16:00	Workshop Overview Cristian Cadar Imperial College London Presentation: video, slides
16:00 – 16:55	Keynote: Adversarial Symbolic Execution for Detecting Timing Side-Channel Leaks Chao Wang University of Southern California, USA Presentation: video, slides
16:55 – 17:00	Break
17:00 – 17:53	Session 1 - Memory Representation and Constraint Solving chair: Tomasz Kuchta, Samsung
	17:00 – 17:15 Relocatable Addressing Model for Symbolic Execution David Trabish , Noam Rinetzky Tel Aviv University, Israel Presentation: video, slides 📹
	17:15 – 17:30 Fine-grain Memory Object Representation in Symbolic Execution Martin Nowack Imperial College London, United Kingdom Presentation: video, slides
	17:30 – 17:45 Caching Results from KLEE’s Independent Solver Zikai Liu , Steven Lumetta ZJU-UIUC Institute, China; University of Illinois at Urbana-Champaign, USA Presentation: video, slides
	17:45 – 17:53 Discussion
17:53 – 18:05	Break
18:05 – 19:15	Session 2 - Testing Evolving Software and Fault Injection chair: Alastair Reid, Google
	18:05 – 18:20 Extending KLEE to Support Automated Behavioral Regression Testing Richard Rutledge , Xinyu Lui, Alessandro Orso Georgia Institute of Technology, USA Presentation: video, slides 📹
	18:20 – 18:35 Automating Function Selection for Patch Testing via Chopped Symbolic Execution Jordy Ruiz , Martin Nowack, Ahmed Zaki, Cristian Cadar Imperial College London, United Kingdom Presentation: video, slides
	18:35 – 18:50 KLEE-Assisted Code Robustness Evaluation against Fault Injections Mounier Laurent, Cristian Ene, Marie-Laure Potet, Etienne Boespflug VERIMAG, France; Université Grenoble Alpes, France Presentation: video, slides
	18:50 – 19:05 Characterizing and Improving Bug-Finders with Automated Bug Injection Yu Hu , Zekun Shen, Brendan Dolan-Gavitt New York University, USA Presentation: video, slides 📹
	19:05 – 19:15 Discussion
19:15 – 19:20	Break
19:20 – 20:30	Session 3 - New Applications chair: Alessandro Orso, Georgia Tech
	19:20 – 19:35 Experimentations with KLEE on FuzzBench Laurent Simon Google, USA Presentation: video, slides
	19:35 – 19:50 An Application of KLEE to Aerospace Industrial Software Juan Francisco García , Daniel Jurjo, Fernando Macías, José F. Morales, Alessandra Gorla IMDEA Software Institute, Spain Presentation: video, slides
	19:50 – 20:05 Effective Testing of Safety-Critical Softwares with KLEE Elson Kurian , Daniela Briola, Pietro Braione, Giovanni Denaro University of Milano-Bicocca, Italy Presentation: video, slides
	20:05 – 20:20 Detecting MPI Usage Anomalies via Partial Program Symbolic Execution Fangke Ye , Jisheng Zhao, Vivek Sarkar Georgia Institute of Technology, USA Presentation: video, slides 📹
	20:20 – 20:30 Discussion

Day Two: 11 June 2021

09:25 – 09:30	Day Overview
09:30 – 10:23	Session 4 - Mutation Testing and Fault Localization chair: Sébastien Bardin, Université Paris-Saclay
	09:30 – 09:45 Killing Stubborn Mutants with Symbolic Execution Thierry Titcheu Chekam , Mike Papadakis, Maxime Cordy, Yves Le Traon University of Luxembourg, Luxembourg Presentation: video, slides
	09:45 – 10:00 The KLEEMA Prototype Sangharatna Godboley , Monika Rani Golla, Arpita Dutta National Institute of Technology Warangal, India; Indian Institute of Technology Kharagpur, India Presentation: video, slides 📹
	10:00 – 10:15 FLASX: A Fault Localization Assistant System Using KLEE Symbolic Execution for Embedded Software Phan Thi Thanh Huyen , Yasufumi Suzuki, Naoto Sato, Masumi Kawakami Hitachi, Japan 📹
	10:15 – 10:23 Discussion
10:23 – 10:30	Break
10:30 – 11:23	Session 5 - Scalability and Side Channels chair: Daniel Schemmel, RWTH Aachen
	10:30 – 10:45 TracerX: Dynamic Symbolic Execution with Interpolation Joxan Jaffar, Rasool Maghareh , Sangharatna Godboley, Xuan-Linh Ha National University of Singapore, Singapore Presentation: video, slides
	10:45 – 11:00 Running Symbolic Execution Forever Frank Busse , Martin Nowack, Cristian Cadar Imperial College London, United Kingdom Presentation: video, slides 📹
	11:00 – 11:15 Efficient Relational Symbolic Execution for Constant-Time at Binary-Level with Binsec/Rel Lesly-Ann Daniel , Sébastien Bardin, Tamara Rezk Université Paris-Saclay, France; INRIA Sophia-Antipolis, France Presentation: video, slides 📹
	11:15 – 11:23 Discussion
11:23 – 11:30	Break
11:30 – 12:23	Session 6 - Model Learning and Education chair: Julien Vanegue, Bloomberg
	11:30 – 11:45 Extracting a Micro State Transition Table Using KLEE Norihiro Yoshida , Takahiro Shimizu, Ryota Yamamoto, Hiroaki Takada Nagoya University, Japan Presentation: video, slides
	11:45 – 12:00 Grey-Box Learning of Register Automata in C Bharat Garhewal , Frits Vaandrager Radboud University, Netherlands
	12:00 – 12:15 Timely Feedback on Assembly Assignments Using KLEE Zikai Liu, Tingkai Liu , Qi Li, Wenqing Luo, Steven Lumetta ZJU-UIUC Institute, China; University of Illinois at Urbana-Champaign, USA Presentation: video, slides
	12:15 – 12:23 Discussion
12:23 – 12:30	Break
12:30 – 13:40	Session 7 - Extending Applicability chair: Martin Nowack, Imperial College London
	12:30 – 12:45 Using KLEE with Large Rust Programs Alastair Reid , Shaked Flur Google Research, United Kingdom Presentation: video, slides 📹
	12:45 – 13:00 Open-Source C++ Support for KLEE Felix Rath , Klaus Wehrle RWTH Aachen University, Germany Presentation: video, slides
	13:00 – 13:15 Get Rid of Inline Assembly Through Verification-Oriented Lifting Frédéric Recoules , Sébastien Bardin, Richard Bonichon, Laurent Mounier, Marie-Laure Potet Université Paris-Saclay, France; Université Grenoble Alpes, France Presentation: video, slides 📹
	13:15 – 13:30 The Long Road towards Testing Multi-Threaded Programs with KLEE Daniel Schemmel , Julian Büning, David Laprell, Klaus Wehrle RWTH Aachen University, Germany Presentation: video, slides
	13:30 – 13:40 Discussion