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 (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 11 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0c286ee Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T09:35:29+01:00
Download 00dafaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-11-30T05:07:52+01:00
Download 2315417 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-04T00:41:44+01:00
Download 8ce0aa2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2023-12-17T03:20:16+01:00
Download d1392d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 6 2023-12-18T01:57:08+01:00
Download c1a56a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 9 2023-12-02T14:20:14Z
Download d29333c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness PredatorHP 4 2023-11-30T08:24:05Z
Download 7a56938 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T12:37:58Z
Download 9d84694 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 9 2023-11-29T02:54:39Z
Download b980be4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T18:15:23+01:00
Download 6a41ace Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T21:15:14

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

Trying to find witnesses for program (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 10 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download db6784f Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T07:09:15+01:00
Download 6b4cef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2022-12-10T20:05:41+01:00
Download 06d1dc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-11T23:25:03+01:00
Download 9548489 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2022-12-25T13:29:58+01:00
Download 103266e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 6 2022-12-09T02:52:26+01:00
Download 5ca4c31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 9 2022-12-14T13:30:33Z
Download 60c656b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:25:44Z
Download 7b04d9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 9 2022-12-13T16:00:30Z
Download 42bc941 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T23:33:37+01:00
Download e64b598 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T14:11:20

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

Trying to find witnesses for program (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1fbe3da Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T05:59:02

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

Trying to find witnesses for program (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0afaa7a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T10:02:05

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

Trying to find witnesses for program (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84500bc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:49 CET (comp)

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

Trying to find witnesses for program (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 030bb2f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:32 CET (sv-comp)

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

Trying to find witnesses for program (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a2534e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T16:03 CET (sv-comp)
Download 21b6880 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 20 2017-12-01T13:03 CET (sv-comp)

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

Trying to find witnesses for program (68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe, sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-termination.c.i, 68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/68763c9a2179c48c1fc2989bd19031bbd8829c13b9c8eeaf244defd8aef53cfe.json

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