KLEE Workshop 2018

Day One: 19 April 2018

08:30 – 09:00	Registration and coffee
09:00 – 09:30	Introduction: A Short History of KLEE + Workshop Overview Cristian Cadar Imperial College London
09:30 – 10:20	Academic keynote: Leveraging Symbolic Execution to Reproduce Field Failures and Mimic User Behavior Alessandro Orso Georgia Institute of Technology, USA
10:20 – 10:45	Coffee Break
10:45 – 11:55	Constraint solving chair: Abhik Roychoudhury
	10:45 – 11:08 Choosing the Best Solver for Your Query Oscar Soria Dustmann, Felix Rath, Philipp Martin, Klaus Wehrle RWTH Aachen University, Germany
	11:08 – 11:31 KLEE’s Solver Chain Revisited – Opportunities for Improvement? Heinrich Kießling, Martin Nowack TU Dresden, Germany
	11:31 – 11:54 Efficient Reuse of Path Condition Solutions by Heuristically Matching Solution Spaces Andrea Aquino, Giovanni Denaro, Mauro Pezzè University of Milano-Bicocca, Italy and University of Lugano, Switzerland
11:55 – 12:10	Poster introductions chair: Martin Nowack
	11:55 – 11:58 Resilience Evaluation via Symbolic Fault Injection on Intermediate Code Hoang M. Le, Vladimir Herdt, Daniel Große, Rolf Drechsler University of Bremen, Germany
	11:58 – 12:01 HASE: Hardware-Assisted Symbolic Execution Jörg Thalheim, Pramod Bhatotia, Pedro Fonseca, Baris Kasikci University of Edinburgh, UK, University of Washington, USA, and University of Michigan, USA
	12:01 – 12:04 Symbolic Execution in Selfie: A First Step Clement Poncelet Salzburg University, Austria
	12:04 – 12:07 Debugging P4 Programs with Vera Costin Raiciu, Dragos Dumitrescu, Matei Popovici, Lorina Negreanu, Radu Stoenescu University Politehnica of Bucharest, Romania
	12:07 – 12:10 Symbolic Execution Projects from the Software Reliability Group Software Reliability Group Imperial College London, United Kingdom
12:10 – 13:45	Lunch & Poster session
13:45 – 14:31	Scalable forms of symbolic execution chair: Indradeep Ghosh
	13:45 – 14:08 The Tracer-X System Joxan Jaffar, Rasool Maghareh National University of Singapore, Singapore
	14:08 – 14:31 Chopped Symbolic Execution David Trabish, Andrea Mattavelli, Noam Rinetzky, Cristian Cadar Tel Aviv University, Israel and Imperial College London, United Kingdom
14:35 – 15:15	Industry keynote: ConcFuzzer: A Sanitizer Guided Hybrid Fuzzing Framework Leveraging Greybox Fuzzing and Concolic Execution Peng Li Baidu, USA
15:15 – 15:40	Coffee Break
15:40 – 16:26	Coverage chair: Frank Busse
	15:40 – 16:03 Advanced Test Coverage Criteria: Specify and Measure, Cover and Unmask Sebastien Bardin, Nikolai Kosmatov CEA LIST, France
	16:03 – 16:26 Towards Efficient Data Flow Test Input Generation Using KLEE Chengyu Zhang, Ting Su, Yichen Yan, Ke Wu, Geguang Pu East China Normal University, Nanyang Technological University and National Trusted Embedded Software Engineering Technology Research Center, China
16:30 – 17:20	Academic keynote: Symbolic Execution for Directed Search and Specification Inference Abhik Roychoudhury National University of Singapore, Singapore
17:30 – 19:30	Reception at the Union Bar

Day Two: 20 April 2018

08:30 – 09:00	Coffee
09:00 – 09:50	Academic keynote: Enhancing Symbolic Execution Using Test Ranges Sarfraz Khurshid University of Texas at Austin, USA
09:54 – 10:40	Symbolic heap and pointers chair: Timotej Kapus
	09:54 – 10:17 Symbolic Execution with Heap Inputs Pietro Braione, Giovanni Denaro, Mauro Pezzè University of Milano-Bicocca, Italy and University of Lugano, Switzerland
	10:17 – 10:40 A Pointer Tracking Memory Model for Symbolic Execution Felix Rath, Daniel Schemmel, Oscar Soria Dustmann, Klaus Wehrle RWTH Aachen University, Germany
10:40 – 11:05	Coffee break
11:05 – 12:14	Scalability chair: Alessandro Orso
	11:05 – 11:28 Evaluating Manual Intervention to Address the Challenges of Bug Finding with Symbolic Execution John Galea, Sean Heelan, Daniel Neville, Daniel Kroening University of Oxford, United Kingdom
	11:28 – 11:51 HASE: Hardware-Assisted Symbolic Execution Jörg Thalheim, Pramod Bhatotia, Pedro Fonseca, Baris Kasikci University of Edinburgh, UK, University of Washington, USA, and University of Michigan, USA
	11:51 – 12:14 Caterpillar: Iterative Concolic Execution for Stateful Programs Laurent Simon, Shuying Liang, Amir Rahmati Samsung Research America, USA
12:14 – 13:20	Lunch
13:20 – 14:06	Fuzzing chair: Peng Li
	13:20 – 13:43 Reviewing KLEE’s Sonar-Search Strategy in Context of Greybox Fuzzing Saahil Ognawala, Alexander Pretschner, Thomas Hutzelmann, Eirini Psallida, Ricardo Nales Amato Technical University of Munich, Germany
	13:43 – 14:06 Feeding the Fuzzers with KLEE Marek Zmysłowski Samsung Poland R&D Institute, Poland
14:10 – 15:00	Industry keynote: Utilization and Evolution of KLEE-based Technologies for Embedded Software Testing at Fujitsu Indradeep Ghosh Fujitsu, USA
15:00 – 15:25	Coffee break
15:25 – 16:34	New application domains chair: Sarfraz Khurshid
	15:25 – 15:48 Probabilistic Symbolic Execution Antonio Filieri Imperial College London, United Kingdom
	15:48 – 16:11 Symbolic Execution Equivalence and Its Applicability to Network Verification Costin Raiciu, Dragos Dumitrescu, Radu Stoenescu University Politehnica of Bucharest, Romania
	16:11 – 16:34 ExpoSE: Practical Symbolic Execution of Standalone JavaScript Blake Loring, Duncan Mitchell, Johannes Kinder Royal Holloway, University of London, United Kingdom
16:40 – 17:00	Closing