Scholarlink

EmergenTheta is our sandbox for emerging analyses within the Theta framework. Previously established analyses have been migrated to Theta, and EmergenTheta focuses exclusively on novelties for both counterexample-guided abstraction refinement over control-flow automata and reachability analyses over symbolic transition systems. The 2026 submission presents a combined predicate–explicit abstraction domain, multithreaded symbolic transition system encodings, on-the-fly reachability and counterexample generation for generalized saturation, and an IC3 backend. This is the first year that we were able to submit EmergenTheta to all categories, representing a significant step in the evolution of Theta, and the competition results indicate the practical viability of the new techniques.

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

EmergenTheta: Experimental Analyses within the Theta Framework (Competition Contribution)

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Milán Mondok,
  • Csanád Telbisz,
  • Levente Bajczi,
  • Dániel Kovács,
  • Mihály Dobos-Kovács,
  • Vince Molnár

摘要

EmergenTheta is our sandbox for emerging analyses within the Theta framework. Previously established analyses have been migrated to Theta, and EmergenTheta focuses exclusively on novelties for both counterexample-guided abstraction refinement over control-flow automata and reachability analyses over symbolic transition systems. The 2026 submission presents a combined predicate–explicit abstraction domain, multithreaded symbolic transition system encodings, on-the-fly reachability and counterexample generation for generalized saturation, and an IC3 backend. This is the first year that we were able to submit EmergenTheta to all categories, representing a significant step in the evolution of Theta, and the competition results indicate the practical viability of the new techniques.