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 (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.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 (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.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 (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.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 (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.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 (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 12 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f98294b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:41 CET (comp)
Download 8d933d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:20:09+01:00 Download 171a40b
Download 0b64ce7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:17:38+01:00 Download ef59de2
Download 2ca52dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:46+01:00 Download 4a54cbb
Download 5a45efa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:51:16+01:00 Download fbfe063
Download c380e6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T02:01:36+01:00 Download be7608f
Download 9aa33da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:13:22+01:00 Download 3c08fe6
Download 7102dc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:44+01:00 Download f98294b
Download 98e2b5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T17:15:28+01:00 Download 120a3b4
Download 120a3b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 35 2019-11-29T19:28:45+01:00
Download 171a40b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 35 2019-12-01T12:35:45+01:00
Download e48a669 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:15 CET (comp)

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

Trying to find witnesses for program (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 12 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c67e7f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T03:33 CET (sv-comp)
Download 2da313c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T22:43 CET (sv-comp)
Download 9e3282c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 35 2018-12-07T23:18:43+01:00
Download 96c07b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:24:39+01:00 Download 66b6a55
Download 29275b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T21:21:12+01:00 Download 54aa061
Download 43d254a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:11:15+01:00 Download 65f374d
Download 63a3316 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:53:50+01:00 Download 2da313c
Download c716e27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:38:53+01:00 Download abec4cf
Download 9c280a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:23:41+01:00 Download aeba186
Download 660b26f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 35 2018-12-06T00:06:29+01:00
Download 20f9935 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T14:17 CET (sv-comp)
Download 41b7115 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T22:44 CET (sv-comp)

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

Trying to find witnesses for program (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 15 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2fd1913 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T05:08 CET (sv-comp)
Download 867218c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:36:25.416369
Download f760021 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:52:14.481776
Download 5af2037 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T18:20:24.497896
Download 128d295 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T18:48:19.072659
Download 916ecd1 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 7412de9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:25:23+01:00 773ccc4
Download 400e093 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:53:53+01:00 665a5cb
Download 22ba919 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T07:51:34+01:00 862f725
Download 671f10f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:46:23+01:00 68f3035
Download fff4f62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T07:23:29+01:00 df61895
Download a6a8def Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 20 2017-12-01T07:01:41+01:00 c70b43c
Download b5f70b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 35 2017-11-30T13:00:39+01:00
Download 5ed1ca8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 1335 2017-11-30T14:22 CET (sv-comp)
Download 7e77b68 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 1335 2017-12-01T19:09 CET (sv-comp)

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

Trying to find witnesses for program (4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6, sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/array_true-unreach-call4_true-termination.i, 4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4a815fa096313d32181b7a8f8f37a181a6c44550f8eb4ad138c01a075cbb61b6.json

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