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/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c
programSHA bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-termination.Problem02_label45_false-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 193699c2545e3272e907febbf391525ede1138cde46a2fba3f4fa3c4e4b40b9e

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/193699c2545e3272e907febbf391525ede1138cde46a2fba3f4fa3c4e4b40b9e.json

Key Value
architecture 32bit
creationtime 2018-12-08T01:05:26+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
programfile ../../sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c
programhash bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/193699c2545e3272e907febbf391525ede1138cde46a2fba3f4fa3c4e4b40b9e.graphml
witness-sha256 193699c2545e3272e907febbf391525ede1138cde46a2fba3f4fa3c4e4b40b9e
witness-size 359162
witness-type violation_witness

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

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

Trying to find witnesses for program (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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 (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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 (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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 (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.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 (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 69403b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 23:22:00
Download f3ea91c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 56 2019-12-03T23:22 CET (comp)
Download 9f68987 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 174 2019-12-11T21:52:23+01:00 Download 4f1d23a
Download ab68c28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 174 2019-12-11T21:09:25+01:00 Download 69403b3
Download 3e79208 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 231 2019-12-11T20:54:57+01:00 Download bcbbd7f
Download 26df7bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 174 2019-12-11T20:44:28+01:00 Download f4f5dc2
Download b9d6963 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 175 2019-12-08T01:51:34+01:00 Download a684466
Download bffcf41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 221 2019-12-04T02:58:09+01:00 Download f3ea91c
Download 1430222 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 174 2019-12-03T08:10:37+01:00 Download d56a932
Download d56a932 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 173 2019-11-29T19:47:54+01:00
Download 4f1d23a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 174 2019-12-01T02:03:50+01:00
Download 96f022d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T21:48:51+01:00 Download 6193671
Download 8664e58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-08T00:28:25+01:00 Download 48a8d40
Download 18e8c05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T21:19:25+01:00 Download 63e29cb
Download 64c7bb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T20:21:32+01:00 Download cfae369
Download 2e6ae19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:35:20+01:00 Download 9a73bba
Download f964169 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-01 11:41:03
Download 8f10be8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-30T08:10:38+01:00
Download 3610e06 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-12-01T00:36:30+01:00

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

Trying to find witnesses for program (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 45a57fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-07T22:17 CET (sv-comp)
Download 546045c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 7 2018-12-08T05:07:37
Download c6d1ea1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 65 2018-12-07T14:36 CET (sv-comp)
Download ef42f20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 174 2018-12-06T12:56:20+01:00
Download 03461a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 175 2018-12-10T20:34:51+01:00 Download 3225786
Download ce8a782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 208 2018-12-09T18:21:34+01:00 Download 75f7657
Download db46ef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 175 2018-12-08T23:44:07+01:00 Download 45a57fa
Download 3604469 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 174 2018-12-08T22:08:40+01:00 Download 546045c
Download d28e316 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 174 2018-12-08T08:48:07+01:00 Download ef42f20
Download 5a624d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 232 2018-12-08T05:02:02+01:00 Download 9308eba
Download eba9074 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 221 2018-12-07T17:44:50+01:00 Download c6d1ea1
Download 96c527d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 174 2018-12-06T10:19:21+01:00 Download 13a835e
Download 8b2ab7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 174 2018-12-06T09:48:08+01:00 Download 0ac5026
Download d8d2d31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 229 2018-12-06T09:15:13+01:00 Download 02530d2
Download 0ac5026 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 174 2018-12-05T19:30:01+01:00
Download d1855e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:53:19+01:00 Download 1c6567c
Download 00a3320 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:40:16+01:00 Download 21d7812
Download 37885e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:35:48+01:00 Download 319b0d3
Download b18fce5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:42:08+01:00 Download cc5ab1a
Download 193699c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-08T01:05:26+01:00
Download f714265 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:25:23+01:00
Download 0b564f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:48:05+01:00
Download be36ebe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-05T05:58:20+01:00

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

Trying to find witnesses for program (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cab93d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-02T22:50 CET (sv-comp)
Download f6e875f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 140 2017-12-03T03:23Z
Download 811067a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:23 CET (sv-comp)
Download 2d03f6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 140 2017-12-02T02:48Z
Download 1dfa9f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T21:41:39.325433
Download a664a03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T08:24:33.054255
Download 09d217b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 11 2017-12-01T16:53 CET (sv-comp)
Download 9ecac11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 11 2017-11-30T23:07 CET (sv-comp)
Download 15eb832 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 100 2017-12-01T00:37:59+01:00
Download 9f949b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 246 2017-11-30T13:30:09+01:00
Download b8f86ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 72 2017-11-30T21:11 CET (sv-comp)
Download 81fce28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 140 2017-12-02T16:13Z
Download 4df0a6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 73 2017-12-01T00:02 CET (sv-comp)
Download 2722214 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T15:01:55+01:00
Download 8a956e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:12Z
Download 5dee5f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T12:56 CET (sv-comp)

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

Trying to find witnesses for program (bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b, sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c, bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bcfba7479b0ab905c2cabbf94a226fe4f8c8b7855211192be51a674b74972d6b.json

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