Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c
programSHA 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
witnessName results-validated/cpa-seq-validate-violation-witnesses-smack.2018-12-08_2205.logfiles/sv-comp19_prop-reachsafety.token_ring.09_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA c7a48bb31d13fab1259dd37160c150953dda20ced3b05d025ca163cc2e479e71

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/c7a48bb31d13fab1259dd37160c150953dda20ced3b05d025ca163cc2e479e71.json

Key Value
architecture 32bit
creationtime 2018-12-08T22:10:50+01:00
inputwitnesshash 39ba51e86e157c9d67e81185471058917d46758904f75435faf65a3b5789800e
producer CPAchecker 1.7-svn 29852
program-sha256 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
programfile ../../sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c
programhash 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c7a48bb31d13fab1259dd37160c150953dda20ced3b05d025ca163cc2e479e71.graphml
witness-sha256 c7a48bb31d13fab1259dd37160c150953dda20ced3b05d025ca163cc2e479e71
witness-size 519030
witness-type violation_witness

This witness was created for this program (cf. table above, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3).

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 10 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6332be2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 519 2019-12-11T21:59:19+01:00 Download 9c0aa75
Download 3847529 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1755 2019-12-11T20:54:26+01:00 Download 133c474
Download 997bffa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 619 2019-12-11T20:44:44+01:00 Download 410268b
Download 7625e6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 519 2019-12-03T08:10:36+01:00 Download 8541383
Download 8541383 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 497 2019-11-30T10:45:15+01:00
Download 9c0aa75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 519 2019-12-01T00:27:58+01:00
Download 38538c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 121 2019-12-08T01:52:23+01:00 Download 5754996
Download 943b353 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 121 2019-12-05T20:20:32+01:00 Download 40dad27
Download 72ca642 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 324 2019-11-30T13:45:26+01:00
Download 5bf9c5d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 324 2019-11-30T23:48:31+01:00

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 15 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7bf7e2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T20:54 CET (sv-comp)
Download 39ba51e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 66 2018-12-08T08:32:07
Download ff90901 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 523 2018-12-07T00:19:00+01:00
Download a254120 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 519 2018-12-09T17:58:04+01:00 Download 144c6f5
Download b62d17e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 520 2018-12-08T23:44:45+01:00 Download 7bf7e2a
Download c7a48bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 519 2018-12-08T22:10:50+01:00 Download 39ba51e
Download ebbd606 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 519 2018-12-08T08:02:59+01:00 Download ff90901
Download a9dc2e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 519 2018-12-08T05:03:32+01:00 Download 6f1d25a
Download 51860ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 519 2018-12-06T09:49:04+01:00 Download 8b43c2b
Download c93f84a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 556 2018-12-06T09:10:33+01:00 Download d36547f
Download 8b43c2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 498 2018-12-06T05:18:39+01:00
Download 8cba782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 121 2018-12-10T20:35:10+01:00 Download 0b5a8e5
Download 6213b30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 121 2018-12-06T10:19:10+01:00 Download 7f31543
Download ff39e8a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 324 2018-12-07T06:48:46+01:00
Download 25f37da Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T01:46:36+01:00

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 9 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f9fbe2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 263 Sat Dec 2 23:53:30 2017
Download 694b94b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T17:40 CET (sv-comp)
Download 85dba9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 20 2017-12-01T20:13:57.489833
Download 711bc99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 20 2017-12-01T19:19:07.537684
Download 66030ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 188 2017-12-01T16:13 CET (sv-comp)
Download 9ef8231 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 188 2017-11-30T20:16 CET (sv-comp)
Download 2b792a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 450 2017-11-30T16:19:36+01:00
Download 81389ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 281 2017-12-01T00:10 CET (sv-comp)
Download b5b5cea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 322 2017-12-01T16:57:00+01:00

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3, sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.09_false-unreach-call_false-termination.cil.c, 00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/00ff1cfee32ce2d3a1261b504e67ec08dcd0f0d4c17d3c30695124a9acc108d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness