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.07_false-unreach-call_false-termination.cil.c
programSHA 0b506ac7059dce1a10a283e5d1f31e269fc1ffec1acc4908ce2a8a42a9476bc5
witnessName results-validated/cpa-seq-validate-violation-witnesses-depthk.2018-12-06_1002.logfiles/sv-comp19_prop-reachsafety.token_ring.07_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA 096d8d349e9af5914266a34b6b74c8265ec2e4384bb252e36a91be0a92d9542e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T10:19:42+01:00
inputwitnesshash 2204df0f4f366e304cf49e941d9e11f67132c7ed324e449342ada347289693cb
producer CPAchecker 1.7-svn 29852
program-sha256 0b506ac7059dce1a10a283e5d1f31e269fc1ffec1acc4908ce2a8a42a9476bc5
programfile ../../sv-benchmarks/c/systemc/token_ring.07_false-unreach-call_false-termination.cil.c
programhash 0b506ac7059dce1a10a283e5d1f31e269fc1ffec1acc4908ce2a8a42a9476bc5
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/096d8d349e9af5914266a34b6b74c8265ec2e4384bb252e36a91be0a92d9542e.graphml
witness-sha256 096d8d349e9af5914266a34b6b74c8265ec2e4384bb252e36a91be0a92d9542e
witness-size 100830
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bd8d20d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 5 2019-12-01 20:41:17
Download b02e723 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 364 2019-12-11T21:54:15+01:00 Download af47111
Download a7c5b77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 364 2019-12-11T21:09:05+01:00 Download bd8d20d
Download 4473e45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1194 2019-12-11T20:55:05+01:00 Download 4dceffe
Download d667fbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 374 2019-12-11T20:44:47+01:00 Download 920d033
Download bd1a94a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 364 2019-12-03T08:05:20+01:00 Download 84b9b59
Download 84b9b59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 351 2019-11-30T14:30:10+01:00
Download af47111 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 364 2019-11-30T21:19:00+01:00
Download 8feb023 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 101 2019-12-08T01:51:22+01:00 Download 73bcca0
Download 0e2b596 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 101 2019-12-05T20:20:31+01:00 Download 0c9572b
Download dcdcbb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 225 2019-11-29T17:33:15+01:00
Download bd2dd49 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 225 2019-12-01T01:37:41+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f38d3c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T06:05 CET (sv-comp)
Download 92826e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 49 2018-12-08T00:55:26
Download 59d6b25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 368 2018-12-07T10:43:46+01:00
Download e9a5b78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 373 2018-12-09T18:14:19+01:00 Download 3d17f47
Download 46674f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 365 2018-12-08T23:44:35+01:00 Download f38d3c4
Download ba799b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 364 2018-12-08T22:09:41+01:00 Download 92826e6
Download 984d20e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 364 2018-12-08T07:53:17+01:00 Download 59d6b25
Download 26ff23a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 364 2018-12-08T05:03:20+01:00 Download 57181a7
Download c13d364 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 364 2018-12-06T09:48:01+01:00 Download f60871e
Download c6e38f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 400 2018-12-06T09:19:24+01:00 Download 8924564
Download f60871e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 351 2018-12-06T01:23:02+01:00
Download 95558a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 101 2018-12-10T20:36:09+01:00 Download 6e64365
Download 096d8d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 101 2018-12-06T10:19:42+01:00 Download 2204df0
Download f0fbc19 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 225 2018-12-07T17:50:40+01:00
Download 47cffa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 225 2018-12-05T13:36:59+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 87eb0f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 187 Sat Dec 2 21:26:58 2017
Download 9d395b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T16:50 CET (sv-comp)
Download 8086806 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 18 2017-12-01T12:09:39.545556
Download 60104cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 16 2017-12-01T08:20:44.306799
Download 32d82c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 94 2017-12-01T21:23 CET (sv-comp)
Download e88fb15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 94 2017-11-30T17:44 CET (sv-comp)
Download b97a006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 318 2017-12-01T01:45:52+01:00
Download 4aa9253 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 194 2017-11-30T13:37 CET (sv-comp)
Download dd3e4cf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 224 2017-12-01T16:07:49+01:00
Download b502761 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 90 2017-12-03T11:13Z

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

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

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

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