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 (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.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 (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.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 (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.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 (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.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 (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.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 (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 26 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bf0f32e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T05:23 CET (sv-comp)
Download 49fa837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T06:39:30
Download 1a32c83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2018-12-06T23:23 CET (sv-comp)
Download 33fe5fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-08T04:22:40+01:00
Download 9397997 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T20:37:31+01:00 Download ff4ec5a
Download eb6fdd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T21:23:33+01:00 Download c703a73
Download 95bdcee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:53:07+01:00 Download d34f3fe
Download 0d08d06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:38:41+01:00 Download cb9e3b2
Download cfa43ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:28:02+01:00 Download 034b255
Download 7807c7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T18:20:23+01:00 Download 725166b
Download 27d0d5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:43:49+01:00 Download bf0f32e
Download c6ea9bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T22:08:36+01:00 Download 49fa837
Download 6319678 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T09:05:31+01:00 Download 33fe5fe
Download e7f6ef3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:03:38+01:00 Download 6a64cbc
Download c30f332 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T03:56:46+01:00 Download 62e95e2
Download 4b65d25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T18:48:09+01:00 Download b06206e
Download 542dda3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T17:43:20+01:00 Download 1a32c83
Download 31203d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T01:17:53+01:00 Download 0fb324c
Download 0eaae8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:19:04+01:00 Download 92c1737
Download 56cae41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:47:56+01:00 Download 8d222a7
Download 35d6d4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:42:46+01:00 Download d969a83
Download 09acbe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:11:09+01:00 Download 8d4f420
Download 8d222a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T00:46:31+01:00
Download df1d21d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:16:50+01:00 Download 618d552
Download 6cde6d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:25 CET (sv-comp)
Download 0317284 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:37 CET (sv-comp)

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

Trying to find witnesses for program (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 22 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c674f89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:13 CET (sv-comp)
Download 6e014ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 6 Sat Dec 2 23:41:57 2017
Download 49067f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 7 2017-12-03T02:25Z
Download 0d8f68f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T04:25 CET (sv-comp)
Download f66d2df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 7 2017-12-02T12:51Z
Download 8111e03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T22:14:40.520160
Download f30467e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T19:40:20.043908
Download c25d788 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T18:58 CET (sv-comp)
Download 0b7fc17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-11-30T19:27 CET (sv-comp)
Download 7305bd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T14:19:49+01:00
Download 32b7524 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 12 2017-11-30T19:21:18+01:00
Download e104ed2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-12-01T01:29:53+01:00
Download c4f66fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T02:57:30+01:00
Download e6fde29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 6 2017-12-01T00:33 CET (sv-comp)
Download 7b220db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 7 2017-12-02T03:56Z
Download ba97187 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 6 2017-11-30T13:17 CET (sv-comp)
Download cf2607d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T21:46 CET (sv-comp)
Download 4c79683 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:04:59.626130
Download aaa77eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:42:57.060272
Download d4de1bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:36:55+01:00 1009665
Download bd79bdb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T16:24 CET (sv-comp)
Download a4d731d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 11 2017-12-01T12:26 CET (sv-comp)

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

Trying to find witnesses for program (1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340, sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json

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