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 (9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994, sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c).

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

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

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

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

Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e896319 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-02 05:04:22
Download f7e338b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 69 2019-12-03T22:18 CET (comp)
Download 81fbabe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 204 2019-12-11T21:45:37+01:00 Download a86cf6c
Download 2008791 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 203 2019-12-11T21:09:35+01:00 Download e896319
Download a3272ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 204 2019-12-11T20:55:08+01:00 Download db6647b
Download d5bea90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 204 2019-12-11T20:44:49+01:00 Download a5f5765
Download 51a4ce5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 205 2019-12-08T01:51:25+01:00 Download 9c5c7cc
Download ad97aff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 257 2019-12-04T02:58:30+01:00 Download f7e338b
Download 52511ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 204 2019-12-03T08:09:46+01:00 Download 4cbd708
Download 4cbd708 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 202 2019-11-30T03:25:29+01:00
Download a86cf6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 203 2019-12-01T16:50:53+01:00
Download 9b69c27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T21:52:32+01:00 Download ddd18ed
Download 7dc0acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-08T00:27:15+01:00 Download ea9a66e
Download b829193 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T21:15:01+01:00 Download 9a9afb7
Download 056ffea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T20:21:35+01:00 Download 659beba
Download 5e92688 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T19:35:09+01:00 Download 45f97b1
Download 04ea9d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 339 2019-11-30T06:51:00+01:00
Download 2fc6156 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 339 2019-12-01T12:44:54+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 173e408 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T01:25 CET (sv-comp)
Download 2b9eda2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 10 2018-12-08T07:15:43
Download 7ff2042 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 80 2018-12-07T12:12 CET (sv-comp)
Download 190cdb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 203 2018-12-07T21:55:14+01:00
Download 3c4da55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 205 2018-12-10T20:36:27+01:00 Download da32c0a
Download c221c0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-09T18:21:54+01:00 Download f778ba1
Download 5bed680 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 207 2018-12-08T23:44:40+01:00 Download 173e408
Download e78a83d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-08T22:10:15+01:00 Download 2b9eda2
Download 5bb341e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-08T08:58:18+01:00 Download 190cdb1
Download 4b94c76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T05:06:36+01:00 Download c40b651
Download 57a2065 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 257 2018-12-07T17:43:57+01:00 Download 7ff2042
Download 59747df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-06T10:20:05+01:00 Download 24f0724
Download 80b906c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-06T09:48:49+01:00 Download 2c93a9c
Download bc99b00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 257 2018-12-06T09:13:59+01:00 Download f683275
Download 2c93a9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 202 2018-12-05T12:28:10+01:00
Download 93f16d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:53:39+01:00 Download 65a87a7
Download 3d27876 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:36:52+01:00 Download 082fd93
Download d711952 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:33:32+01:00 Download cd507e1
Download 961edc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:42:02+01:00 Download d6e9ddb
Download ef6ad8a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 339 2018-12-07T19:03:11+01:00
Download 169e7c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-08T07:59:24+01:00
Download ad24eaf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T09:49:07+01:00
Download fe94585 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 327 2018-12-06T00:04:59+01:00

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

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

Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7a422b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-02T20:18 CET (sv-comp)
Download ca42a29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T00:04 CET (sv-comp)
Download 39b74cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 176 2017-12-02T10:46Z
Download 1ff57d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T22:43:04.703813
Download 9d53063 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T08:25:56.869698
Download 89ed45d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 14 2017-12-01T15:54 CET (sv-comp)
Download 809d0a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 14 2017-12-01T04:41 CET (sv-comp)
Download 5f2f453 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 117 2017-11-30T15:52:21+01:00
Download e8c96d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 300 2017-11-30T14:21:48+01:00
Download 0dd5c13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 112 2017-11-30T16:01:52+01:00
Download 5220894 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 182 2017-12-02T00:29:39+01:00
Download 1a8f74d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 88 2017-11-30T22:16 CET (sv-comp)
Download 69317e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 176 2017-12-02T06:11Z
Download 81513a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 89 2017-11-30T20:11 CET (sv-comp)
Download 9a66756 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 31 2017-12-01T16:51 CET (sv-comp)

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

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

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

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