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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c
programSHA 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
witnessName results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.Thun_true-termination_true-valid-memsafety.c.files/witness.graphml
witnessSHA 0e2cf6c5be622dbafd53d9eca162e36b0d0186f4850d6a0192f6b327ab4695d2

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/0e2cf6c5be622dbafd53d9eca162e36b0d0186f4850d6a0192f6b327ab4695d2.json

Key Value
architecture 32bit
creationtime 2017-12-01T16:25 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_a1edc672-f474-4e36-a66e-0071268aefea/sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c
programhash 840ba140d54545c25f92f53e7838cceec95e9821
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0e2cf6c5be622dbafd53d9eca162e36b0d0186f4850d6a0192f6b327ab4695d2.graphml
witness-sha256 0e2cf6c5be622dbafd53d9eca162e36b0d0186f4850d6a0192f6b327ab4695d2
witness-size 5480
witness-type correctness_witness

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 5 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 87c84b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T10:54:14Z
Download a5121a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T20:19:53Z
Download aebb817 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T21:27:35
Download 1b67766 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 21 2023-12-17T11:07:49+01:00
Download 446cbc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T14:15:36Z

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 6 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6d032e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T09:53:25Z
Download 0bd272a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-18T20:50:31Z
Download 6d23d66 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T11:37:32Z
Download a460406 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T15:30:45
Download d90af96 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 21 2022-12-08T10:42:58+01:00
Download 8517d24 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T18:22:22Z

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0c072b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T05:11:09Z
Download f8ecf68 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T15:47:11Z
Download 83149bd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T05:24:54
Download 0f61034 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 21 2021-12-06T02:08:39+01:00

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5311402 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T16:17:48
Download 678e962 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T22:06:49
Download f2303c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T10:28:32

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5d6cfbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 6 2019-11-30T04:29:51+01:00
Download 5fda9af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6 2019-12-01T00:27:15+01:00
Download 94d2a35 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:08 CET (comp)

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 2 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 49d5005 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:04 CET (sv-comp)
Download 133a462 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T15:22 CET (sv-comp)

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e2fecf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:44:42.970490
Download 1731f24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:38:16.565864
Download 0e2cf6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T16:25 CET (sv-comp)
Download d513ac3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 24 2017-12-01T18:12 CET (sv-comp)

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

Trying to find witnesses for program (7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0, sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Thun_true-termination_true-valid-memsafety.c, 7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7a7e4c1bea4db860aff2cd2a7b7cbb6b10c52fe15286dfe6b897761cc9d83fd0.json

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