Skip to content

Witnesses: emit YAML 2.3 violation witnesses #45

Closed

Description

@nils-loose

SV-COMP 2027 requires YAML violation witnesses, format 2.3+ for Java; GraphML is no longer listed (benchmarks). Correctness witnesses are not expected.

WitnessCreator (repo, v0.1.1) only writes GraphML.

  • Emit witness.yml (entry_type: violation_sequence, format_version: "2.3", language: Java, sha256 input_file_hashes, no data_model)
  • One function_return waypoint per Verifier.nondet*() call (location = closing ), \result == <literal>), final target at the violating statement
  • Columns: the [WITNESS] markers only carry line numbers today
  • Release a new WitnessCreator version, bump WITNESS_CREATOR_VERSION/SHA in .github/workflows/gradle.yml
  • Validate locally (Local witness validation: use pinned SV-COMP 2027 validators #47)

Refs: Java guide, schema, example examples/java/ExDarko_false.witness-2.3.yml. Watch sv-witnesses !120 (2.4 changes function_return to ext_java_expression).

Activity

  1. added this to the SV-COMP 2027 milestone on Oct 15, 2026
  2. nils-loose commented on Oct 20, 2026

    @nils-loose
    ContributorAuthor

    Done in #58: witness.yml (YAML 2.x violation witness) is written from the trace by witnesscreator v1.0.0. Merged into dev through #92. Validation against the competition validators remains in #47.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions