Contributions

Opening Remarks

Cristian Cadar (Imperial College London)
Presentation: slides video

Accepted Presentations

• Concretely Mapped Symbolic Memory Locations for Memory Error Detection
  Haoxin Tu (Singapore Management University, Singapore), Lingxiao Jiang (Singapore Management University), Jiaqi Hong (Independent Researcher), Xuhua Ding (Singapore Management University), He Jiang (Dalian University of Technology)
  Presentation: slides video

• Symbolic Grammar Mining
  Leon Bettscheider (CISPA Helmholtz Center for Information Security), Andreas Zeller (CISPA Helmholtz Center for Information Security)

• Find Your Path: SoK on Path Selection Strategies in Symbolic Execution
  Dairo De Ruck (DistriNet - KU Leuven), Jorn Lapon (DistriNet - KU Leuven), Vincent Naessens (DistriNet - KU Leuven)
  Presentation: slides video

• Program Repair Guided by Datalog-defined Static Analysis
  Yu Liu (National University of Singapore), Sergey Mechtaev (University College London), Pavle Subotic (Fantom Foundation), Abhik Roychoudhury (National University of Singapore)
  Presentation: slides video

• Automating Differential Testing with Over-approximate Symbolic Execution
  Richard Rutledge (Georgia Institute of Technology), Alessandro Orso (Georgia Institute of Technology)
  Presentation: slides video

• Deterministic State-space Exploration: Comparing and Measuring Effectiveness of Symbolic Execution Implementations
  Martin Nowack (Imperial College London)
  Presentation: slides video

• An Efficient Black-box Support of Advanced Coverage Criteria for KLEE
  Nicolas Berthier (OCamlPro), Steven de Oliveira (OCamlPro), Nikolai Kosmatov (Thales Research & Technology), Delphine Longuet (Thales Research & Technology), Romain Soulat
  Presentation: slides video

• What’s Up from Below? An Overview of Recent Advances in BINSEC
  Frédéric Recoules (CEA, List), Sébastien Bardin (CEA LIST, University Paris-Saclay)
  Presentation: slides video

• Concolic Program Repair
  Ridwan Salihin Shariffdeen (National University of Singapore), Yannic Noller (Singapore University of Technology and Design), Lars Grunske (Humboldt-Universität zu Berlin), Abhik Roychoudhury (National University of Singapore)
  Presentation: slides video

• Complex Test Input Generation in KLEE
  Alexey Babushkin, Aleksandr Misonizhnik, Yurii Kostyukov (RnD Toolchain Labs, Huawei), Dmitry Mordvinov (Huawei), Dmitry Ivanov (Huawei)
  Presentation: slides video

• Symbolic Execution Oriented Constraint Solving
  Zhenbang Chen (National University of Defense Technology), Ziqi Shuai (National University of Defense Technology), Yufeng Zhang (Hunan University), Zehua Chen (College of Computer, National University of Defense Technology), Guofeng Zhang (Hunan University), Jun Sun (Singapore Management University), Wei Dong (National University of Defense Technology), Ji Wang
  Presentation: slides video

• Concurrent Adversarial Separation Logic: A General Approach to Under-approximate Reasoning about Concurrent Programs
  Azalea Raad (Imperial College London), Julien Vanegue (Bloomberg, USA), Josh Berdine (SkipLabs), Peter O’Hearn (University College London, UK and Lacework, London, UK)
  Presentation: slides video

• State Merging with Quantifiers in Symbolic Execution
  David Trabish (Tel Aviv University), Noam Rinetzky (Tel Aviv University), Sharon Shoham (Tel Aviv University), Vaibhav Sharma (Amazon)
  Presentation: slides video

• Accelerating Symbolic Execution by Targeted Control-flow Transformations
  Charitha Saumya (Purdue University), Rohan Gangaraju (Purdue University), Kirshanthan Sundararajah (Virginia Tech), Milind Kulkarni (Purdue University)

• Deferring Branches to Speed Up Symbolic Execution
  Eric Lu, Eddie Kohler (Harvard University)
  Presentation: slides video

• How the SHA-3 Buffer Overflow Was Found using KLEE
  Nicky Mouha (Strativia / NIST Associate)
  Presentation: slides video

• State Merging for Concolic Testing of Event-driven Applications
  Maarten Vandercammen, Coen De Roover (Vrije Universiteit Brussel)
  Presentation: slides video

• Symbolic Execution of Binary Code based on Formal ISA Semantics
  Sören Tempel (University of Bremen), Tobias Brandt (Independent), Christoph Lüth (University of Bremen / DFKI GmbH), Rolf Drechsler (University of Bremen / DFKI GmbH)
  Presentation: slides video

• Automated Generation of Database Mocks with Symbolic Execution
  Cesar Cornejo (University of Rio Cuarto and CONICET), Agustín Borda (Dept. of Computer Science FCEFQyN, University of Rio Cuarto), Nazareno Aguirre (University of Rio Cuarto and CONICET, Argentina), Marcelo F. Frias (The University of Texas at El Paso), Pablo Ponzio (Dept. of Computer Science FCEFQyN, University of Rio Cuarto), Germán Regis (University of Rio Cuarto and CONICET)
  Presentation: slides video

• Precise Lazy Initialization for Programs with Complex Heap Inputs
  Juan Manuel Copia (IMDEA Software Institute; Universidad Politécnica de Madrid), Facundo Molina (IMDEA Software Institute), Nazareno Aguirre (University of Rio Cuarto and CONICET, Argentina), Marcelo F. Frias (The University of Texas at El Paso), Alessandra Gorla (IMDEA Software Institute), Pablo Ponzio (Dept. of Computer Science FCEFQyN, University of Rio Cuarto)
  Presentation: slides video

Accepted Posters

• Exploring Complexity Estimation with Symbolic Execution and Large Language Models
  *Adrians Skapars (University of Manchester), Youcheng Sun (University of Manchester), Yannic Noller (Singapore University of Technology and Design), Corina S. Păsăreanu (NASA Ames and Carnegie Mellon University)
  Presentation: slides

• FastKLEE: Faster Symbolic Execution via Reducing Redundant Bound Checking of Type-safe Pointers
  Haoxin Tu (Singapore Management University, Singapore), Lingxiao Jiang (Singapore Management University), Xuhua Ding (Singapore Management University), He Jiang (Dalian University of Technology)
  Presentation: slides video

• TracerX - Pruning Dynamic Symbolic Execution with Weakest Precondition Interpolation
  Arpita Dutta (National University of Singapore), Rasool Maghareh (Huawei), Joxan Jaffar (National University of Singapore)
  Presentation: slides video

• SC-MCC Test Case Generation using Dynamic Symbolic Execution Engines
  Golla Monika Rani, Sangharatna Godboley (National Institute of Technology Warangal), Joxan Jaffar (National University of Singapore), Rasool Maghareh (Huawei)
  Presentation: slides video

• Mixed Fixed-point and Floating-point Symbolic Execution
  Thom Hughes (Imperial College London), Daniel Schemmel (Imperial College London), Martin Nowack (Imperial College London), Cristian Cadar (Imperial College London)
  Presentation: slides video

• Towards Complete Fuzzing with KLEE
  Kanika Gupta (National Institute of Technology, Warangal), Sangharatna Godboley (National Institute of Technology Warangal)
  Presentation: slides video

• Input Grammar Oriented Symbolic Execution
  Ke Ma, Yunlai Luo (National University of Defense Technology), Weijiang Hong (National University of Defense Technology, Changsha, China), Zhenbang Chen (National University of Defense Technology), Yufeng Zhang (Hunan University), Ji Wang
  Presentation: slides video

Closing Remarks

Cristian Cadar (Imperial College London)
Presentation: slides video