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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ad39b8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T20:24:51+01:00 Download a6926a4
Download 2bd26be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T20:16:41+01:00 Download bfc8d6d
Download a1cc96c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T20:02:20+01:00 Download b068898
Download e837bb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-08T00:36:36+01:00 Download 568e183
Download 03e4e89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T23:28:59+01:00 Download d192f33
Download 705f69a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T19:42:38+01:00 Download a4e1882
Download f3c584c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T19:02:54+01:00 Download db1dce9
Download 028fcf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-11-30T16:55:18+01:00 Download a209c27
Download a209c27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 287 2019-11-30T11:11:21+01:00
Download bfc8d6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 287 2019-12-01T17:31:02+01:00
Download 0dc8ebf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 339 2019-11-30T05:31:31+01:00
Download 60796eb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 339 2019-11-30T23:50:18+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 564e6be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:46:14
Download 372d616 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 287 2018-12-08T00:42:51+01:00
Download 98d14ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-10T19:59:47+01:00 Download 4099312
Download 209e49c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:31:24+01:00 Download 41030cc
Download f6915e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:07:51+01:00 Download 50458b6
Download 1519fb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T19:49:39+01:00 Download e283c3a
Download 9b4c23e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-08T21:34:49+01:00 Download 564e6be
Download 85a72ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-08T07:08:38+01:00 Download 372d616
Download 5efb547 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-08T03:05:39+01:00 Download 8971515
Download 28425cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:29:10+01:00 Download 0642013
Download 2a6fe9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T08:45:56+01:00 Download 2672b34
Download 08515b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T08:07:20+01:00 Download 666de35
Download 2672b34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-05T21:42:34+01:00
Download 6ecb919 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 339 2018-12-08T04:21:29+01:00
Download 507fa1d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-08T08:58:37+01:00
Download 9889706 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T09:48:59+01:00
Download 746288b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 327 2018-12-06T01:13:16+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 44584e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 184 2017-12-02T05:39Z
Download 64f6c3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download 9d1cc24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-03T03:57:47+01:00 05d06a0
Download f1706f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-03T02:51:25+01:00 60994a5
Download 50ec6d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-02T23:55:08+01:00 98cc05d
Download e57426d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-02T15:19:30+01:00 bb26b95
Download 18d79d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T06:36:15+01:00 3f344f1
Download d175e12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T06:02:53+01:00 124a5f8
Download 924224c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T06:02:27+01:00 db97d59
Download 4442aa2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-12-01T05:17:10+01:00 4a7e641
Download b6c93b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 287 2017-11-30T23:12:45+01:00
Download b477641 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 489 2017-12-01T00:08:26+01:00
Download 14b97ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 287 2017-11-30T12:20:32+01:00
Download ef979fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 455 2017-12-02T08:14:35+01:00
Download 872e524 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 160 2017-12-02T02:00Z
Download d8f7bd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 778 2017-11-30T20:26 CET (sv-comp)
Download 29b9e73 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 315 2017-12-01T17:46:58+01:00
Download 6db1c70 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 31 2017-12-01T12:58 CET (sv-comp)

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

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

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

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