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 (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

Found 7 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2dd4a12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:40:16Z
Download 70aa587 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:21:57+01:00
Download f6487f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 1d976ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T19:16:05
Download 42ca9de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 3649 2023-12-20T02:42:20+01:00 Download 1d976ad
Download d913621 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 3649 2023-12-03T18:47:33+01:00 Download 70aa587
Download c9264fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4129 2023-11-30T08:27:41+01:00

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

Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

Found 8 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fe1bec4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T12:57:37Z
Download 8ef1686 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:00:39+01:00
Download f6487f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download f6cdaf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T12:44:18
Download 0433702 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4832 2023-01-29T11:46:42+01:00 Download f6487f2
Download 59b3df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4650 2023-01-28T23:06:33+01:00 Download 8ef1686
Download 7b0c62e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 523 2023-01-28T17:49:35+01:00 Download fe1bec4
Download 937bb02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6029 2022-12-10T17:09:44+01:00

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

Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

Found 5 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ba6da8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T19:58:21Z
Download 5fdf00c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:36:01+01:00
Download ab6c948 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2021-12-09T07:10:52
Download 3cfb64b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6029 2021-12-09T12:40:36+01:00
Download 5d5520c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T16:17:03

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

Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

Found 6 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9299be2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:40:36
Download b474c5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2020-12-08T10:24:07
Download fd73c5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6029 2020-12-05T13:50:46+01:00
Download e2b88a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6029 2020-12-08T04:35:26+01:00
Download f0004ad Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T18:24:49
Download b9b0bae Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T02:33:22

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

Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

Found 1 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6553356 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6015 2019-12-01T02:26:34+01:00

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

Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

Found 1 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f2feb85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T18:15:31

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

Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c, de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cacd77e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 7 2017-12-01T13:21 CET (sv-comp)
Download 648d136 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-12-01T21:14 CET (sv-comp)

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

Trying to find witnesses for program (de5b7f1cccf5c7fe435559014125bbfd73538586d5303d45f8d606cb31a4b74b, sv-benchmarks/c/termination-numeric/rec_counter1_true-termination_true-no-overflow.c).

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

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