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 (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 24 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e1fc3c3 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T09:51:57+01:00
Download ff4b435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T23:12:46Z
Download 6d1e2d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-11-30T04:54:54+01:00
Download dc552d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T18:07:47+01:00
Download 14c699e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-19T02:09:09+01:00
Download 413f7a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 6 2023-12-18T02:16:03+01:00
Download 8364e77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T10:18:40Z
Download 00543c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T13:24:50Z
Download 012a69b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T20:25:04Z
Download 802fc33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T12:50:49Z
Download cecd785 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 11 2023-12-02T12:08:16Z
Download 0a5a87e 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:25:39Z
Download 87ffebe 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:45:56Z
Download a74e31c 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 Kojak 11 2023-12-02T22:13:06Z
Download 5a44f33 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 Goblint (tags/svcomp24-0-gc2e9465a7) 7 2023-12-01T01:43:53Z
Download 8ea0380 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 CBMC 19 2023-12-17T13:53:45+01:00
Download 558ebef 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 11 2023-11-28T23:41:56Z
Download 2ab83e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T14:09:59Z
Download 1cdb03a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T21:57:15Z
Download 49813f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T22:56:06
Download c3670b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 19 2023-12-17T10:19:16+01:00
Download bda049c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T08:08:20Z
Download 3d88eff Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T13:06:16Z
Download 95ad47d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T20:44:41Z

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

Trying to find witnesses for program (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 19 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c792124 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T05:10:42+01:00
Download 85b1004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2022-12-10T19:40:30+01:00
Download fb6c6d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T02:49:24+01:00
Download 73e6482 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T00:09:03+01:00
Download 073405a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 6 2022-12-09T02:58:42+01:00
Download 0b91272 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T19:18:53Z
Download 15823df Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T23:24:25Z
Download ec08a96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T11:57:43Z
Download 70743b8 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 11 2022-12-14T14:06:24Z
Download 3a65c8d 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-11T11:17:55Z
Download 2c53e73 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 Kojak 11 2022-12-14T20:23:03Z
Download b582ba1 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 CBMC 19 2022-12-08T06:12:39+01:00
Download cfd07ef 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 11 2022-12-13T17:11:29Z
Download 9f0f103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T08:24:59Z
Download e948a72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-18T23:24:26Z
Download ca1779a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T10:52:03Z
Download aa2d1c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T14:08:45
Download ba811ca Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 19 2022-12-08T05:30:29+01:00
Download 840cf35 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T19:42:41Z

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

Trying to find witnesses for program (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 4 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b9135a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T05:04:52Z
Download 219fc55 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T14:15:14Z
Download 51f5cfe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T06:34:49
Download 875b3ad Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 18 2021-12-06T10:50:19+01:00

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

Trying to find witnesses for program (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 3 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3231057 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T23:55:45
Download 59dccb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T20:07:16
Download a32930b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T08:28:12

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

Trying to find witnesses for program (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cf50b80 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:41 CET (comp)

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

Trying to find witnesses for program (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ea056c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T16:00 CET (sv-comp)
Download 9be139b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T23:54 CET (sv-comp)

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

Trying to find witnesses for program (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 5 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a10eee7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:08:29.534920
Download 8835c7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:16:27.560996
Download 87439fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T21:07 CET (sv-comp)
Download 43f6928 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 19 2017-12-01T16:09 CET (sv-comp)
Download 736e5d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 19 2017-12-01T12:07 CET (sv-comp)

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

Trying to find witnesses for program (337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89, sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json

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