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.08_false-unreach-call_false-termination.cil.c
programSHA a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8
witnessName results-validated/cpa-seq-validate-violation-witnesses-veriabs.2018-12-10_2034.logfiles/sv-comp19_prop-reachsafety.token_ring.08_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA 955638a1aafc938b575722d0eb2516c208195685aa4c69b5b4839477e866a022

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T20:37:46+01:00
inputwitnesshash fe07d85924945aca6aec25767eed60bab82f9c2aa2369dcaa84ff18d46a71002
producer CPAchecker 1.7-svn 29852
program-sha256 a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8
programfile ../../sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c
programhash a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/955638a1aafc938b575722d0eb2516c208195685aa4c69b5b4839477e866a022.graphml
witness-sha256 955638a1aafc938b575722d0eb2516c208195685aa4c69b5b4839477e866a022
witness-size 111398
witness-type correctness_witness

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

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

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

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c, a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8.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 (a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8, sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c, a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8.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 (a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8, sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c, a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8.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 (a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8, sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c, a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8.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 (a69b280e69020d71c0f8f7b7fbf247c545cbd18069f7941041c7046d42a94fe8, sv-benchmarks/c/systemc/token_ring.08_false-unreach-call_false-termination.cil.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6116a06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 439 2019-12-11T21:46:22+01:00 Download e4ed870
Download f0b7a0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1462 2019-12-11T20:54:45+01:00 Download b1273c3
Download f7a849d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 439 2019-12-11T20:44:28+01:00 Download 9619c1d
Download 8e8b079 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 439 2019-12-03T08:10:09+01:00 Download 8e562a5
Download 8e562a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 421 2019-11-30T05:10:58+01:00
Download e4ed870 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 438 2019-11-30T23:09:08+01:00
Download 342125c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 111 2019-12-08T01:51:26+01:00 Download 5d3c41e
Download fcc6dbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 111 2019-12-05T20:20:14+01:00 Download 5365f15
Download dff5637 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 274 2019-11-30T01:42:03+01:00
Download e91eb96 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 274 2019-12-01T00:35:16+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 93ef0aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T06:33 CET (sv-comp)
Download 6341e15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 57 2018-12-08T17:56:43
Download 4ef7181 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 442 2018-12-08T01:51:04+01:00
Download 12e4f6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 439 2018-12-09T18:21:22+01:00 Download 4da9610
Download aeb4007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 440 2018-12-08T23:43:36+01:00 Download 93ef0aa
Download 0d36448 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 439 2018-12-08T22:11:12+01:00 Download 6341e15
Download 003c617 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 439 2018-12-08T08:41:23+01:00 Download 4ef7181
Download 581e500 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 439 2018-12-08T05:03:52+01:00 Download 6d3944f
Download 703a018 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 439 2018-12-06T09:48:03+01:00 Download a002944
Download d5fae3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 474 2018-12-06T09:10:29+01:00 Download 713a85a
Download a002944 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 422 2018-12-05T21:44:39+01:00
Download 955638a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 111 2018-12-10T20:37:46+01:00 Download fe07d85
Download 3a74b46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 111 2018-12-06T10:13:35+01:00 Download ab13566
Download a55465c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 274 2018-12-08T03:55:24+01:00
Download 45428be Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 274 2018-12-06T07:06:53+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 86237c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 221 Sun Dec 3 00:48:52 2017
Download 6d1285a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:54 CET (sv-comp)
Download bbc263b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 24 2017-12-02T05:11:31.891593
Download c89b865 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 18 2017-12-01T07:50:04.486073
Download a949038 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 102 2017-12-01T15:55 CET (sv-comp)
Download 49d038e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 102 2017-12-01T05:55 CET (sv-comp)
Download e3d8b23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 382 2017-11-30T18:45:13+01:00
Download 4e187bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 230 2017-12-01T02:53 CET (sv-comp)
Download 40844c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 272 2017-12-01T12:56:34+01:00

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

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

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

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