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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c331a9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:03:02Z
Download 9ac5b0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T18:02:20+01:00
Download 5e598c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:38 CET (comp)
Download 0fff0b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T23:51:15
Download 55b55a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4472 2023-12-20T03:55:40+01:00 Download 5e598c7
Download 61c992e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4130 2023-11-30T06:03:48+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3f2b1fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T13:46:23Z
Download dbed781 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:04:36+01:00
Download 5e598c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T10:59 CET (comp)
Download 3cdcd71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T15:14:41
Download dab66c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4833 2023-01-29T11:46:34+01:00 Download 5e598c7
Download 91796bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4650 2023-01-29T05:05:49+01:00 Download 3cdcd71
Download 34fafdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5020 2023-01-28T23:07:53+01:00 Download dbed781

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ea0fe17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T21:03:32Z
Download 8aec4ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T14:19:52+01:00
Download c601df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2021-12-09T07:05:29
Download 8724d1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6030 2021-12-08T19:02:05+01:00
Download cd65592 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6030 2021-12-09T09:56:30+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cfda7b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:35:22
Download f4d57c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2020-12-08T11:06:08
Download bfa8a43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6030 2020-12-05T16:23:31+01:00
Download 6403972 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6030 2020-12-08T00:24:48+01:00

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eee59ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:15:56
Download f002659 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6681 2018-12-08T02:29:30+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7ff0b52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 7 2017-12-01T14:05 CET (sv-comp)
Download 4c8143e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-12-01T21:43 CET (sv-comp)

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

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

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

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