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/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i
programSHA 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
witnessName results-validated/cpa-seq-validate-violation-witnesses-cbmc.2018-12-06_0859.logfiles/sv-comp19_prop-memsafety.sll-queue_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml
witnessSHA cce89feca3a547e95c307c5e290c10a0ac334817da81c6fba68bc2ee85d8bc4f

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/cce89feca3a547e95c307c5e290c10a0ac334817da81c6fba68bc2ee85d8bc4f.json

Key Value
architecture 32bit
creationtime 2018-12-06T09:18:33+01:00
inputwitnesshash b48a4fb3f1a6742d984f8c145247cb7e58fd8f9db2293d8a2251ebd5579c13cb
producer CPAchecker 1.7-svn 29852
program-sha256 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
programfile ../../sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i
programhash 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memcleanup) )
witness-file witnessFileByHash/cce89feca3a547e95c307c5e290c10a0ac334817da81c6fba68bc2ee85d8bc4f.graphml
witness-sha256 cce89feca3a547e95c307c5e290c10a0ac334817da81c6fba68bc2ee85d8bc4f
witness-size 20434
witness-type correctness_witness

This witness was created for this program (cf. table above, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6).

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

Trying to find witnesses for program (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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 (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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 (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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 (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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 (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 22 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 59e2685 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 2 2019-12-01 13:50:57
Download c9c4e46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 20 2019-12-11T21:50:22+01:00 Download 9c5541d
Download 53a548e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 21 2019-12-11T21:09:09+01:00 Download 59e2685
Download 07bd561 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 20 2019-12-08T00:07:36+01:00 Download b5c0fac
Download 7b519f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 20 2019-12-03T08:08:37+01:00 Download ac5ebd4
Download ac5ebd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 19 2019-11-30T04:01:55+01:00
Download 9c5541d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 19 2019-12-01T16:39:39+01:00
Download c0be9a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 23:35:22
Download e4db163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-11T21:45:10+01:00 Download 2d3772c
Download f06d82a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-11T20:55:11+01:00 Download c631585
Download 5b3ed24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-08T00:06:06+01:00 Download f9cfa9c
Download ea92810 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-07T21:16:58+01:00 Download d4f88b2
Download d6acd20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-03T08:56:54+01:00 Download 6dffe2a
Download d0baf3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 26 2019-11-30T13:26:39+01:00
Download 6f643d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 8 2019-12-07T12:03:30+01:00
Download 744b156 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 26 2019-12-01T06:27:49+01:00
Download 4afdb58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:40:24+01:00 Download 744b156
Download 510ef77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:09:25+01:00 Download c0be9a0
Download b80fbd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T20:45:59+01:00 Download d30b2f5
Download f1c7e76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 21 2019-12-08T01:51:46+01:00 Download 6f643d7
Download 9dcafc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 21 2019-12-05T20:20:13+01:00 Download 2a72d7a
Download 8787137 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 21 2019-12-03T08:08:46+01:00 Download d0baf3e

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

Trying to find witnesses for program (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 29 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 61164d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T11:16 CET (sv-comp)
Download 4ee312e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 3 2018-12-08T15:51:19
Download a634d21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-08T23:42:23+01:00 Download 61164d9
Download a640ad3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-08T22:10:48+01:00 Download 4ee312e
Download 035c624 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-07T09:26:52+01:00 Download 3db8ce3
Download a296c1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-06T10:19:10+01:00 Download 9aaa724
Download c167de0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:48:54+01:00 Download 29d9b79
Download 29d9b79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T05:23:05+01:00
Download cce89fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:18:33+01:00 Download b48a4fb
Download a54df21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T10:34 CET (sv-comp)
Download 5f7be1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T19:26:30
Download fd24fba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 8 2018-12-10T19:03:28+01:00
Download ccd0fdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 25 2018-12-07T23:01:06+01:00
Download d2b8bcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-10T10:48:49+01:00 Download 63bb772
Download 2fa1710 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-09T20:37:54+01:00 Download 058cb3f
Download 6730d4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-09T20:18:45+01:00 Download d33c6a3
Download e28c323 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-08T22:10:53+01:00 Download 5f7be1b
Download c1bbe00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-08T04:53:00+01:00 Download 0e5c529
Download 646c38e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-08T04:26:16+01:00 Download 63bb772
Download 463154b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-07T09:13:10+01:00 Download 159eca1
Download 8a204c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-06T10:19:14+01:00 Download f179af7
Download 0f30ad9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-06T09:08:41+01:00 Download ed82537
Download 4b5a4fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-05T22:39:49+01:00
Download 7bd241c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-10T20:36:17+01:00 Download fd24fba
Download dc56ef7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-09T18:21:35+01:00 Download fe2057b
Download 7f8dfe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T23:43:14+01:00 Download a54df21
Download e2d634e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T08:49:16+01:00 Download ccd0fdb
Download 6af62e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-07T01:22:27+01:00 Download 048e9c9
Download 9871f1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:48:37+01:00 Download 4b5a4fc

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

Trying to find witnesses for program (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 11 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 19986d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T07:40 CET (sv-comp)
Download 159eca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 6 2017-12-01T20:46 CET (sv-comp)
Download 050a1a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 21 2017-12-02T10:01Z
Download 4180031 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 12 2017-12-01T17:45 CET (sv-comp)
Download d88a46a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 6 2017-12-01T20:26:06.684831
Download a627b22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 7 2017-12-01T13:52:19.303359
Download 43a4a68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-11-30T22:44 CET (sv-comp)
Download 5cdc9d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 24 2017-11-30T16:55:49+01:00
Download 6d1d782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T20:26:23+01:00
Download 55ae228 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 16 2017-12-02T13:16:41+01:00
Download 8123ad6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 19 2017-11-30T11:25 CET (sv-comp)

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

Trying to find witnesses for program (1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6, sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json

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