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 (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.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 (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.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 (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.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 (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.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 (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 2 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eca88d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T23:27:38+01:00 Download be796a0
Download 44e3d05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T19:45:06+01:00 Download f54f489

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

Trying to find witnesses for program (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 8 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a84afd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T12:35:36
Download def0779 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-07T05:28:38+01:00
Download 291c7b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:35:28
Download 6235b58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:32:41+01:00 Download 6930419
Download f6d75bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:10:49+01:00 Download 0798df3
Download 4aae90c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T21:36:56+01:00 Download 291c7b1
Download 8dc70f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:44:52+01:00 Download 0a4a539
Download b0da024 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:28:41+01:00 Download c489b67

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

Trying to find witnesses for program (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 15 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d08a00a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 11 2017-12-01T14:28 CET (sv-comp)
Download dd44d43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 13 2017-11-30T17:33:04+01:00
Download 5196874 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T23:29:55+01:00
Download f094a6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T05:17:10+01:00
Download 0a4a539 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:41 CET (sv-comp)
Download 5efa1ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 10 2017-12-03T02:28Z
Download b39aa0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 11 2017-12-01T16:07 CET (sv-comp)
Download 0db6e35 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 2e7c806 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 8 2017-12-01T03:29:26+01:00
Download 72ca997 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T07:06:13+01:00 1fa959c
Download 347e603 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T04:19:44+01:00 b75c085
Download 3642280 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T02:34:48+01:00 01a7b78
Download 7d091fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T00:13:45+01:00 5f9833b
Download c7ae2ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T08:13:29+01:00 915f22e
Download 154961a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 10 2017-12-02T06:21Z

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

Trying to find witnesses for program (81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d, sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c, 81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/81e28bb53e01b3a378cc750ca7921d9f8e335397dd22ace52066a9e22f99074d.json

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