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/ldv-regression/test24_true-unreach-call_true-termination.c
programSHA cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
witnessName results-validated/cpa-seq-validate-correctness-witnesses-symbiotic.2018-12-08_2246.logfiles/sv-comp19_prop-reachsafety.test24_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 4da31238204a3415e8844f6c563a6eaa134f76bdae7ab3439ad5d62d74a1c606

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T23:18:00+01:00
inputwitnesshash 7e98bf730c74fc1c893e9ad15e7a937abcd816f57f8a5e4b9fb3d618024772c5
producer CPAchecker 1.7-svn 29852
program-sha256 cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
programfile ../../sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c
programhash cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/4da31238204a3415e8844f6c563a6eaa134f76bdae7ab3439ad5d62d74a1c606.graphml
witness-sha256 4da31238204a3415e8844f6c563a6eaa134f76bdae7ab3439ad5d62d74a1c606
witness-size 6217
witness-type correctness_witness

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

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

Trying to find witnesses for program (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.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 (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.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 (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.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 (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.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 (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7c463fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:19 CET (comp)
Download dfc0dae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:29:57+01:00 Download 427e1d0
Download 6e1703d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:17:32+01:00 Download db5abad
Download 6c5d1ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:07:10+01:00 Download 0f3a88b
Download 5dd7ce3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:22+01:00 Download 317c27f
Download ab31aa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:36:23+01:00 Download 760201c
Download c6efa1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:46:49+01:00 Download 293f20a
Download e2e053c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:44:39+01:00 Download aa4ba99
Download a82083b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T19:40:56+01:00 Download 0cbe70e
Download d3ffdf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T01:42:20+01:00 Download c053bb0
Download 750dd6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:12:50+01:00 Download 590a95a
Download 5bec5ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:58+01:00 Download 7c463fd
Download 70cf3d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T19:54:48+01:00 Download b534533
Download 0779667 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T17:23:32+01:00 Download 37315ad
Download 37315ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T00:47:00+01:00
Download 760201c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 6 2019-12-07T13:17:58+01:00
Download 0f3a88b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-11-30T22:26:33+01:00
Download fd66f7c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:59 CET (comp)

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

Trying to find witnesses for program (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7e98bf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T19:40 CET (sv-comp)
Download 6970766 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T20:02:59
Download d0f28f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T09:36:23+01:00
Download 90be448 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:05:43+01:00 Download 0d1e70c
Download 04f6b45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:34:09+01:00 Download 88a8008
Download 620a37e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T19:48:55+01:00 Download 0988195
Download 6610ed0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T17:22:53+01:00 Download b2859c4
Download 4da3123 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:18:00+01:00 Download 7e98bf7
Download 30b0d8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:35:40+01:00 Download 6970766
Download 5c123be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T06:00:42+01:00 Download d0f28f3
Download 086db51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T02:40:43+01:00 Download cffc4cf
Download baa161e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T02:25:13+01:00 Download 970c8ee
Download 83e4c0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:44:57+01:00 Download 1c993ad
Download 054b8e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T08:52:43+01:00 Download 1f1bfe9
Download 0313337 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:32+01:00 Download a469493
Download 559d751 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:56:16+01:00 Download c1d2cc5
Download bf8e852 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:20:43+01:00 Download 24ea2c2
Download a60c3f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:29:47+01:00 Download 9d0891f
Download c1d2cc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:16:35+01:00
Download e52f648 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T05:35 CET (sv-comp)

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

Trying to find witnesses for program (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 29 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7b5542b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 12 2017-11-30T22:52:13+01:00
Download 760a687 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:14 CET (sv-comp)
Download 7010814 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 9 2017-12-03T02:54Z
Download d30d8ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T18:33 CET (sv-comp)
Download 9b973d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 11 2017-12-02T07:37Z
Download 74c8a4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:12:52.299433
Download 1732117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:33:22.253674
Download 8b4a8b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:36:13.195995
Download 5c2ca7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T15:39:29.152347
Download 4fe4bed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 7 2017-12-01T19:39 CET (sv-comp)
Download eb8f82d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-12-02T23:42:53+01:00
Download ea1b357 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T03:23:22+01:00
Download 74172e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T06:59:52+01:00 286232a
Download 0ea7dc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T04:08:30+01:00 99af053
Download dbc5741 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T01:49:01+01:00 11be26b
Download cf38ecf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T01:05:01+01:00 8a4285b
Download 2bb5a28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:36:21+01:00 6d72bd2
Download 06c0f91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T14:20:09+01:00 fbd9243
Download eefa4cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T08:32:30+01:00 8da582a
Download d72b9b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T00:13:50+01:00 8459e0a
Download 852ebb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:21:41+01:00 d4c75c7
Download 5572af4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:13:58+01:00 d8b6185
Download 5ce7a29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:11:33+01:00 bb69bae
Download 1b52a0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T04:41:49+01:00 48132b2
Download 1ff90e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T02:09:17+01:00
Download 8a1c08a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 6 2017-12-02T01:14:31+01:00
Download a78242f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 13 2017-11-30T13:54 CET (sv-comp)
Download ec4a039 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 9 2017-12-02T19:01Z
Download 29f616c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 12 2017-12-01T15:07 CET (sv-comp)

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

Trying to find witnesses for program (cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba, sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_true-unreach-call_true-termination.c, cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/cc1815e5cb3973c51d39901b33005464c8969226287e77dd46669f2fab66e3ba.json

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