Contributions

Opening Remarks

Cristian Cadar (Imperial College London)
Presentation: slides

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)
  Presentation slides

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

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

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

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

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

• Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery
  Md Shafiuzzaman (UCSB), Achintya Desai (UCSB), Wenbo Guo (UCSB), Tevfik Bultan (UCSB)
  Presentation slides

• 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)
  Presentation slides

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

Accepted Posters

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

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

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