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 (5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31, ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i).

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

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

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

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

Found 6 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i, 5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b3105e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:18:24+01:00 Download 6a3bf59
Download 32734cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:02:58+01:00 Download 21414bf
Download 823dcba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:53:51+01:00 Download 7804888
Download 6ae9014 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:12:48+01:00 Download 4abcfcd
Download 087f330 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-11-30T16:10:19+01:00 Download fd0722e
Download fd0722e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 12 2019-11-29T17:14:46+01:00

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

Trying to find witnesses for program (5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31, ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i).

Found 15 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i, 5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 70ce26c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:47 CET (sv-comp)
Download 5c2c5b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T13:33:09
Download 9abd556 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 12 2018-12-06T13:10:45+01:00
Download 8fc8de8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:21:25+01:00 Download 5e8e5ee
Download f06ee0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:21:29+01:00 Download 7668e7b
Download 1f1503d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:31:31+01:00 Download 70ce26c
Download 10b0f8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T22:03:37+01:00 Download 5c2c5b4
Download 3b4b1a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T05:32:52+01:00 Download 9abd556
Download 87fb71d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T04:12:02+01:00 Download b906e28
Download 64a069c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:58:47+01:00 Download 3a52b71
Download e604896 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:43:50+01:00 Download 580422b
Download 7f67bce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:14:51+01:00 Download 3ffbea5
Download e32220b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T07:55:43+01:00 Download ff3baa2
Download 3ffbea5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-05T10:23:44+01:00
Download 9ee70dd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T09:17 CET (sv-comp)

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

Trying to find witnesses for program (5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31, ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i).

Found 22 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i, 5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0a08938 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 107 2017-11-30T14:10:10+01:00
Download 327b7a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 60 2017-11-30T18:27:22+01:00
Download 3a52b71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:33 CET (sv-comp)
Download be61e0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T15:48 CET (sv-comp)
Download 5d5b37f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:46:06.233816
Download db04ab5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:00:04.019105
Download b484e3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T23:13:00.839517
Download cd5d17d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T11:42:24.747998
Download 8638ad0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 17 2017-12-01T16:49 CET (sv-comp)
Download 9a79a27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 17 2017-11-30T18:28 CET (sv-comp)
Download 29f66cf 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 1eed585 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T04:24:17+01:00 8e2507d
Download 05a3e82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T21:02:40+01:00 faa568b
Download c086d78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T08:02:40+01:00 c04ea4c
Download 7ba5259 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T00:31:10+01:00 ead74a0
Download 8f503f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T22:46:01+01:00 1a6fa77
Download 424e1c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T08:27:56+01:00 8718576
Download 8294a4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T05:53:02+01:00 ebf0f3f
Download b7e88ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 52 2017-11-30T17:45 CET (sv-comp)
Download 60fa5e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 136 2017-12-01T03:40 CET (sv-comp)
Download b40d041 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 52 2017-12-01T13:34 CET (sv-comp)
Download 4d8e23a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 31 2017-12-01T14:58 CET (sv-comp)

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

Trying to find witnesses for program (5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31, ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/max10_true-unreach-call_true-termination.i, 5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5a67df9ec49ed0b6fa6892a451d519e2e9565ab4d7eb8ddc86dc0eb84a18fc31.json

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