Contributions

Accepted Presentations

• A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module
  Dirk Beyer (LMU Munich), Po-Chun Chien (LMU Munich), Bo-Yuan Huang (Intel), Nian-Ze Lee (National Taiwan University), Thomas Lemberger (LMU Munich)

• Agentic Concolic Execution
  Zhengxiong Luo (National University of Singapore), Huan Zhao (National University of Singapore), Dylan Wolff (National University of Singapore), Cristian Cadar (Imperial College London), Abhik Roychoudhury (National University of Singapore)

• Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code
  Dimitrios Stamatios Bouras (Peking University), Sergey Mechtaev (Peking University)

• Empc: Effective Path Prioritization for Symbolic Execution with Path Cover
  Shuangjie Yao (Hong Kong University of Science and Technology and Columbia University), Dongdong She (Hong Kong University of Science and Technology)

• Enhancing Symbolic Execution of Programs for Control Flow Path Feasibility Analysis
  Hovhannes Movsisyan (RAU), Hripsime Hovhannisyan (RAU), Hayk Aslanyan (RAU), Tigran Avagyan (RAU)

• Enhancing Symbolic Execution with Machine-Checked Safety Proofs
  David Trabish (Technion), Shachar Itzhaky (Technion)

• Enhancing Symbolic Execution with Self-Configuring Parameters
  Minjong Kim (Sungkyunkwan University), Sooyoung Cha (Sungkyunkwan University)

• FeatMaker: Automated Feature Engineering for Search Strategy of Symbolic Execution
  Jaehan Yoon (Sungkyunkwan University), Sooyoung Cha (Sungkyunkwan University)

• Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery
  Md Shafiuzzaman (UC Santa Barbara), Achintya Desai (UC Santa Barbara), Wenbo Guo (UC Santa Barbara), Tevfik Bultan (UC Santa Barbara)

• LLM-Driven Generation of Summaries for Symbolic Execution
  Frederico Ramos (INESC-ID and University of Lisbon), João Matos (INESC-ID and University of Lisbon and Instituto de Telecomunicações), Jorge Hristovsky (INESC-ID and University of Lisbon), Pedro Adão (University of Lisbon and Instituto de Telecomunicações), Ruben Martins (Carnegie Mellon University), José Fragoso Santos (INESC-ID and University of Lisbon)

• Selective Concolic Testing
  Guofeng Zhang (National University of Defense Technology), Zhenbang Chen (National University of Defense Technology), Ziqi Shuai (National University of Defense Technology), Jun Sun (Singapore Management University), Weijiang Hong (National University of Defense Technology), Yufeng Zhang (Hunan University), Ji Wang (National University of Defense Technology), Yang Liu (National University of Defense Technology)

• Triggering the Hidden: Oracle Design Meets KLEE for Backdoor Detection
  Michaël Marcozzi (Universite Paris-Saclay and CEA, List)

Accepted Posters

• Automatic Unit-Test Generation Based on Symbolic Execution
  Tigran Avagyan (Russian-Armenian University), Levon Shahbazyan (Russian-Armenian University), Hovhannes Movsisyan (Russian-Armenian University), Hayk Aslanyan (Russian-Armenian University)

• Co-Designing Compiler Infrastructure and Symbolic Execution to Improve SMT-LIB Encoding
  Sören Tempel (Technische Universität Braunschweig), Christian Dietrich (Technische Universität Braunschweig)

• EAR: Debugging Libraries through API Call Traces
  Tongjun Zhang (Imperial College London), Cristian Cadar (Imperial College London)

• Interprocedural Symbolic Static Analysis for Go
  Varvara Dvortsova (ISP RAS), Alexey Borodin (ISP RAS)

• Online Input Grammar Synthesis Aided Symbolic Execution
  Ke Ma (National University of Defense Technology), Yunlai Luo (National University of Defense Technology), Zhenbang Chen (National University of Defense Technology), Weijiang Hong (National University of Defense Technology), Yufeng Zhang (Hunan University), Ji Wang (National University of Defense Technology)