Scholarlink

SWAT is an instrumentation-based dynamic symbolic execution framework for Java programs running on the standard Java Virtual Machine (JVM). The framework’s two main components are the symbolic executor that collects traces during concrete execution and a decoupled symbolic explorer to systematically explore the collected program paths. This paper describes recent improvements made to SWAT for the SV-COMP 2026 Java category including the first-time participation in the new runtime track. To explicitly reason about exceptional program flows, symbolic modelling of instructions that may throw exceptions is introduced into SWAT. Furthermore, various performance optimizations were implemented, including a migration from the theory of arithmetic to the theory of fixed-size bit-vectors for symbolic reasoning. Finally, 124 new symbolic models were added to significantly increase the coverage of supported Java Standard Library methods. Overall these improvements led to a significant increase in SWAT’s performance and capabilities, reaching a shared first place in the valid-assert subcategory and fourth place overall in the Java category.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

SWAT: Improvements to the Symbolic Executor (Competition Contribution)

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Nils Loose,
  • Florian Sieck,
  • Felix Mächtle,
  • Thomas Eisenbarth

摘要

SWAT is an instrumentation-based dynamic symbolic execution framework for Java programs running on the standard Java Virtual Machine (JVM). The framework’s two main components are the symbolic executor that collects traces during concrete execution and a decoupled symbolic explorer to systematically explore the collected program paths. This paper describes recent improvements made to SWAT for the SV-COMP 2026 Java category including the first-time participation in the new runtime track. To explicitly reason about exceptional program flows, symbolic modelling of instructions that may throw exceptions is introduced into SWAT. Furthermore, various performance optimizations were implemented, including a migration from the theory of arithmetic to the theory of fixed-size bit-vectors for symbolic reasoning. Finally, 124 new symbolic models were added to significantly increase the coverage of supported Java Standard Library methods. Overall these improvements led to a significant increase in SWAT’s performance and capabilities, reaching a shared first place in the valid-assert subcategory and fourth place overall in the Java category.