SV-COMP 2027

Issues

• Local witness validation: use pinned SV-COMP 2027 validators

  enhancement
  SWAT-project/SWAT#47 · Filter by author nils-loose opened on Oct 15, 2026 · SV-COMP 2027

• fm-tools: svcomp27 version + participants list

  SWAT-project/SWAT#49 · Filter by author nils-loose opened on Oct 15, 2026 · SV-COMP 2027
  1

• Use the full SV-COMP time and memory budget

  SWAT-project/SWAT#51 · Filter by author nils-loose opened on Oct 15, 2026 · SV-COMP 2027
  3

• Evaluate alternatives to HTTP for executor–explorer communication

  SWAT-project/SWAT#55 · Filter by author nils-loose opened on Oct 15, 2026 · SV-COMP 2027

• Evaluate JVM reuse and parallel exploration

  SWAT-project/SWAT#56 · Filter by author nils-loose opened on Oct 15, 2026 · SV-COMP 2027

• Expected verdicts of PieSegment_true and AlbersProjection_true

  SWAT-project/SWAT#63 · Filter by author nils-loose opened on Oct 15, 2026 · SV-COMP 2027
  3

• Keep sv-benchmarks Java tasks in sync for SV-COMP 2027

  SWAT-project/SWAT#64 · Filter by author nils-loose opened on Oct 15, 2026 · SV-COMP 2027

• Verifier input names can collide between call sites

  SWAT-project/SWAT#85 · Filter by author nils-loose opened on Oct 19, 2026 · SV-COMP 2027

• Explorer accepts traces from another SWAT run on the same port

  SWAT-project/SWAT#91 · Filter by author nils-loose opened on Oct 19, 2026 · SV-COMP 2027

• Move the static property pre-check from the executor into the static pre-analysis

  SWAT-project/SWAT#93 · Filter by author nils-loose opened on Oct 20, 2026 · SV-COMP 2027
  4

• Executor eagerly shadows new arrays: large nondet array sizes cause agent OOM (UNKNOWN)

  SWAT-project/SWAT#97 · Filter by author nils-loose opened on Oct 21, 2026 · SV-COMP 2027
  1

• SA walk desyncs on object ==: the refEquals helper no longer matches the extractor's RefEqualityEmitter

  bug
  SWAT-project/SWAT#100 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027
  1

• Pin branches can never be flipped: tasks using toCharArray, setLength etc. on symbolic input cannot end SAFE

  bug
  SWAT-project/SWAT#101 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027

• Possible false SAFE: System.arraycopy model hides the out-of-bounds path for symbolic-length arrays (unconfirmed)

  bug
  SWAT-project/SWAT#102 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027

• Possible false SAFE in loop-state matching: inherited JDK static members and Math.random bypass the untracked-code check (unconfirmed)

  bug
  SWAT-project/SWAT#103 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027

• Loop-state positions cost quadratic time per trace, also with --no-loop-state-matching

  bug
  SWAT-project/SWAT#104 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027

• Slicing UF definitions and precision loss by symbol kind rely on unenforced invariants

  enhancement
  SWAT-project/SWAT#105 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027

• Integer/Long divideUnsigned and remainderUnsigned have no divisor-is-zero branch (unconfirmed)

  bug
  SWAT-project/SWAT#106 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027

• SA guards: open-ordinal keys count as checked; async-entry list misses fork and parallel streams (unconfirmed)

  bug
  SWAT-project/SWAT#107 · Filter by author solid-eureka opened on Oct 23, 2026 · SV-COMP 2027