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/sizeofparameters_test_true-termination.c_true-unreach-call.i
programSHA 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
witnessName results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.sizeofparameters_test_true-termination.c_true-unreach-call.i.files/witness.graphml
witnessSHA 3798717afdb3a38ad38805cec97f257f5a72242fbf53a165935e8ceee71ef34b

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T00:12 CET (sv-comp)
producer Symbiotic
program-sha256 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
programfile /tmp/vcloud-vcloud-master/worker/working_dir_92df883d-d637-4d38-b93a-00855c98a7a0/sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i
programhash 8ac3f058bb34bbd4b12f3029e0c513ab0cd329ea
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3798717afdb3a38ad38805cec97f257f5a72242fbf53a165935e8ceee71ef34b.graphml
witness-sha256 3798717afdb3a38ad38805cec97f257f5a72242fbf53a165935e8ceee71ef34b
witness-size 775
witness-type correctness_witness

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

Trying to find witnesses for program (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.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 (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.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 (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.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 (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.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 (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 47ec460 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:24:13+01:00 Download f46b183
Download e46a661 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:21:45+01:00 Download 1e48651
Download e9da26c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:17:16+01:00 Download ccc4386
Download b014a9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:16+01:00 Download 776e0a6
Download 868fa7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:45:28+01:00 Download c4a0fc6
Download 36874e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:46:43+01:00 Download e68d788
Download edf1a39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:31:24+01:00 Download f49c948
Download a0fca59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:40:46+01:00 Download 7d351f9
Download 2a72ee3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-06T02:19:51+01:00 Download aefb04f
Download 627d9b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:12:52+01:00 Download 95feb73
Download 4edbf1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:02:57+01:00 Download a944b2b
Download 0a99474 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:02:08+01:00 Download 0d70114
Download 005ecae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T16:25:32+01:00 Download bb828ad
Download bb828ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-29T21:37:29+01:00
Download c4a0fc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T13:22:11+01:00
Download ccc4386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T05:29:28+01:00

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

Trying to find witnesses for program (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 24 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 745eefa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T19:59 CET (sv-comp)
Download f7bff7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T11:06:55
Download e5e7a48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T07:12 CET (sv-comp)
Download 34050cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-08T04:34:14+01:00
Download 9c28cad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T19:51:29+01:00 Download 73f5b6e
Download 9892ebc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:30+01:00 Download 4d28d48
Download e937354 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:29:16+01:00 Download fdbaf08
Download 1b8df1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:48:03+01:00 Download 449afe0
Download d5e1438 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:13:07+01:00 Download fc5d09e
Download 6e18b48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:11:00+01:00 Download 745eefa
Download cadba96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:33:23+01:00 Download f7bff7e
Download ec68ad7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T06:09:41+01:00 Download 34050cd
Download fa2ecae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:03:48+01:00 Download 15cbe85
Download 9cfa466 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:57+01:00 Download 8d2e594
Download 1626508 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:39:22+01:00 Download e5e7a48
Download 6592a47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T08:05:25+01:00 Download e026163
Download 8736fb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T00:45:57+01:00 Download a890678
Download 30f9748 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:35+01:00 Download 0e01cf6
Download 7e8d5e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:45:26+01:00 Download de312a2
Download 1895e27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:24:41+01:00 Download 4865bed
Download 54e3b4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:18:22+01:00 Download e313985
Download de312a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T23:35:35+01:00
Download 7b83471 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:33 CET (sv-comp)
Download d7ff3c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T22:38 CET (sv-comp)

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

Trying to find witnesses for program (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 39 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6a4b35b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:28 CET (sv-comp)
Download bebc186 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 4 2017-12-01T18:13 CET (sv-comp)
Download 8d2e594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:25 CET (sv-comp)
Download c3ccda6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-03T04:12Z
Download 3798717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T00:12 CET (sv-comp)
Download e026163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:54 CET (sv-comp)
Download e61e786 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T06:27Z
Download e5bbac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:48:52.323965
Download a66fb97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:05:16.253294
Download 427d2e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T12:43:48.145815
Download 1445d51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T12:28:20.857866
Download 5c0175b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T21:14 CET (sv-comp)
Download cd208ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-02T19:11:04+01:00
Download bacc767 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T16:57:06+01:00
Download cb06383 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T07:01:57+01:00 e661f2e
Download 6e3b617 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:30:55+01:00 b70b3ab
Download 6ea546d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:06:15+01:00 3dfa1f8
Download a71295f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:02:18+01:00 df58043
Download 5faf924 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:23:28+01:00 645e1f9
Download 834652a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T15:29:44+01:00 6e6162b
Download 6db9a0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:40:07+01:00 8a34af7
Download 3c29f86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:04:41+01:00 091ac28
Download 2de0fa7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:25:28+01:00 4eac837
Download 66cff56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T21:07:04+01:00 3c681e4
Download 5fa3f50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:19+01:00 f2a15dc
Download 87e43fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:41:18+01:00 556674c
Download 6918e2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:13:08+01:00 44017eb
Download 1cc5878 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:03:03+01:00 e2762e6
Download a7cfa4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:48:37+01:00 8a3549c
Download b3790ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:48:32+01:00 cefff01
Download 9e160f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T15:34:38+01:00
Download 4c85b24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T15:45:54+01:00
Download 0db3569 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T19:31:42+01:00
Download 727fcbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-01T23:00:37+01:00
Download 9bdcfcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T14:45 CET (sv-comp)
Download 1bdd7b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T19:33Z
Download 786153a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 9 2017-12-01T00:16 CET (sv-comp)
Download 6849521 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T15:38 CET (sv-comp)
Download 7df3896 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T13:18 CET (sv-comp)

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

Trying to find witnesses for program (27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662, sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i, 27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/27cab329c6ef4160c254ac7cb84669185c864cafdd2bc30a23023df5f5e7d662.json

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