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/test27_true-unreach-call_true-termination.c
programSHA 7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4
witnessName results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.test27_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA d226c384f724c5a44ea74f5754c3cd9c5d74ce0d776893922099ce084782f8c7

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/d226c384f724c5a44ea74f5754c3cd9c5d74ce0d776893922099ce084782f8c7.json

Key Value
architecture 32bit
creationtime 2017-12-01T00:32:29+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4
programfile ../../sv-benchmarks/c/ldv-regression/test27_true-unreach-call_true-termination.c
programhash e697b26a33773e62711271acc7c4dca91991203b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/d226c384f724c5a44ea74f5754c3cd9c5d74ce0d776893922099ce084782f8c7.graphml
witness-sha256 d226c384f724c5a44ea74f5754c3cd9c5d74ce0d776893922099ce084782f8c7
witness-size 7932
witness-type correctness_witness

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

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

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test27_true-unreach-call_true-termination.c, 7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4.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 '19

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

Found 18 witnesses for program sv-benchmarks/c/ldv-regression/test27_true-unreach-call_true-termination.c, 7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7eb56c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:44 CET (sv-comp)
Download 8a7f609 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T01:57:07
Download 09a6254 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 9 2018-12-10T17:17:08+01:00
Download 2a581f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-08T04:16:23+01:00
Download 0bcaf8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-10T20:10:50+01:00 Download 09a6254
Download c8d702f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:00:10+01:00 Download a5ce2f9
Download e2ae9a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T16:54:25+01:00 Download 9a09e3e
Download 55f72bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:18:48+01:00 Download 7eb56c1
Download efe4c41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T21:40:20+01:00 Download 8a7f609
Download 13175ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:36:29+01:00 Download 2a581f9
Download 834501f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T02:51:57+01:00 Download 1138d8b
Download 7f027fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-07T08:53:25+01:00 Download 893ccab
Download eef7b91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:29:04+01:00 Download 9227f79
Download db51dbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:00:59+01:00 Download 08bfaf6
Download 7d565c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T08:19:21+01:00 Download 0090d0c
Download d5f0f7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T07:59:54+01:00 Download d10e99c
Download 08bfaf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-05T23:36:11+01:00
Download f20feab Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:25 CET (sv-comp)

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

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

Found 27 witnesses for program sv-benchmarks/c/ldv-regression/test27_true-unreach-call_true-termination.c, 7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7d53e2ce606e1790b25e6f35e71c7a6080a3728555121fad1f17a0ad8adb17b4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae383db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 40 2017-11-30T13:45:49+01:00
Download 7c383e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:04 CET (sv-comp)
Download 8140f9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T01:50 CET (sv-comp)
Download 7149905 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 26 2017-12-02T07:00Z
Download 6603319 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:07:49.725894
Download 316e2a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:33:12.333934
Download 703bcf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T17:04:44.818942
Download 7617de8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T17:32:08.901787
Download 7e7bb87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T15:26 CET (sv-comp)
Download 58a15f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 9 2017-12-02T18:52:16+01:00
Download b21535b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 9 2017-11-30T17:21:06+01:00
Download e9dfb46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T04:28:48+01:00 5f9b886
Download b879b7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T01:18:46+01:00 8cf2704
Download 1203eba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T00:52:09+01:00 269d54b
Download d75b3d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T20:18:50+01:00 239742c
Download 5351137 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T15:30:43+01:00 902ef74
Download 232714f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T07:43:14+01:00 8a74231
Download a48151a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T00:07:14+01:00 21ce510
Download c11c1e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T22:25:17+01:00 16ae152
Download 0d22ea5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T08:15:55+01:00 c80758d
Download 2bd4802 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T05:44:44+01:00 2f11a76
Download 594570d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T05:41:39+01:00 7f2a474
Download d226c38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T00:32:29+01:00
Download ce8372d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 8 2017-12-01T22:27:28+01:00
Download 416a058 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 26 2017-11-30T17:21 CET (sv-comp)
Download d27569b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 16 2017-12-02T19:09Z
Download 46fe9bd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 26 2017-12-01T14:41 CET (sv-comp)

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

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

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

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