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 (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.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 (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.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 (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.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 (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.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 (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 2 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 079ce67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2019-12-03T22:59 CET (comp)
Download 13028f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:02 CET (comp)

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

Trying to find witnesses for program (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 5 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a5e5345 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T03:24 CET (sv-comp)
Download 119aba8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-06T23:11 CET (sv-comp)
Download 19edf2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 6686 2018-12-05T21:49:15+01:00
Download 06bd8b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T18:21 CET (sv-comp)
Download 697eeab Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T14:35 CET (sv-comp)

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

Trying to find witnesses for program (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 11 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d2a2220 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:33 CET (sv-comp)
Download e318d2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 4 2017-12-02T01:07 CET (sv-comp)
Download 281c744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:32:09.852976
Download eeed682 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-02T06:11:12.988217
Download 957bd2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 6 2017-12-01T14:11 CET (sv-comp)
Download 65683d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 57 2017-12-01T11:57 CET (sv-comp)
Download 053df9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 9 2017-12-03T10:26Z
Download d6e5d1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:55:55.077759
Download 921153d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:12:38.648434
Download 00d7549 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T20:59 CET (sv-comp)
Download 75f4497 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 28 2017-12-01T17:43 CET (sv-comp)

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

Trying to find witnesses for program (4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674, ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-numeric/recHanoi02_true-termination_true-no-overflow.c, 4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4d40c00c11a681795ffe0a38d427ca3917e71d52439dae4623d9b59109c60674.json

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