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 (NUS), Huan Zhao (NUS), Dylan Wolff (NUS), Cristian Cadar (Imperial), Abhik Roychoudhury (NUS)

• 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 (HKUST and Columbia), Dongdong She (HKUST)

• 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 (UCSB), Achintya Desai (UCSB), Wenbo Guo (UCSB), Tevfik Bultan (UCSB)

• LLM-Driven Generation of Summaries for Symbolic Execution
  Frederico Ramos (INESC-ID and U. Lisbon), João Matos (INESC-ID and U. Lisbon and IT), Jorge Hristovsky (INESC-ID and U. Lisbon), Pedro Adão (U. Lisbon and IT), Ruben Martins (CMU), José Fragoso Santos (INESC-ID and U. Lisbon)

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

Accepted Posters

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

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

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

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