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/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i
programSHA aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
witnessName results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-memsafety.dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA 567a1ad877ae900cd847061c4b4b8c057b86e4702eca8030faeee39708b92b38

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T11:55 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
producer CBMC
programfile ../../sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i
programhash b7a6c79ad5924d178a48cf0cbbdc1138caa9a120
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/567a1ad877ae900cd847061c4b4b8c057b86e4702eca8030faeee39708b92b38.graphml
witness-sha256 567a1ad877ae900cd847061c4b4b8c057b86e4702eca8030faeee39708b92b38
witness-size 55769
witness-type correctness_witness

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

Trying to find witnesses for program (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.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 (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.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 (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.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 (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.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 (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 17 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ad9495b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 16 2019-11-30T07:09:16+01:00
Download 64cec9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 16 2019-12-01T00:53:48+01:00
Download aeff736 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:44 CET (comp)
Download c74e42a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:42:52+01:00 Download ec1a1da
Download dc1d99e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:34:55+01:00 Download 2b3da9b
Download 0f411d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:26:15+01:00 Download a48ecb7
Download 23d85ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:17:06+01:00 Download ebb7535
Download 0c3bc20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-08T00:51:25+01:00 Download 1658e42
Download c75f1d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-08T00:01:05+01:00 Download 66d81c4
Download f481c23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-06T02:10:41+01:00 Download d671cce
Download 3e2c4c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-05T19:28:10+01:00 Download 405170a
Download 3f1cc33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-04T02:22:29+01:00 Download aeff736
Download 6536792 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-11-30T20:12:22+01:00 Download e18a18d
Download 7b00b7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-11-30T17:18:35+01:00 Download 50a05c7
Download 50a05c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 55 2019-11-29T16:16:56+01:00
Download 1658e42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 19 2019-12-07T11:00:00+01:00
Download a48ecb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 17 2019-12-01T09:32:49+01:00

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

Trying to find witnesses for program (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 23 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 04a365c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T05:06 CET (sv-comp)
Download 221e72a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 17 2018-12-06T20:53:57+01:00
Download 606c4ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-05T12:47:33+01:00
Download c19970f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:40 CET (sv-comp)
Download 55091ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:29:16
Download 30e56ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T15:43 CET (sv-comp)
Download ae992ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 19 2018-12-10T18:07:37+01:00
Download 0a75135 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 54 2018-12-07T19:10:07+01:00
Download fdca926 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-10T20:13:11+01:00 Download ae992ae
Download a7be699 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-10T10:31:55+01:00 Download ef4f168
Download f246360 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-09T19:41:34+01:00 Download 27efabc
Download 3595f43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T23:21:19+01:00 Download c19970f
Download 817408a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T21:37:52+01:00 Download 55091ec
Download faf580f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-08T06:39:48+01:00 Download 0a75135
Download 6e3a357 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T02:55:16+01:00 Download d39f100
Download 33f7f7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T02:23:07+01:00 Download ef4f168
Download 58b6363 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-07T16:38:47+01:00 Download 30e56ec
Download dbb2f4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-07T08:44:42+01:00 Download 0d3a2c8
Download d6f4f75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:28:49+01:00 Download 9e9526d
Download 791407b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-06T08:56:02+01:00 Download 1a163c0
Download 75ed83b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T08:04:46+01:00 Download 0776fde
Download 7bbf275 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T07:45:09+01:00 Download bbea6ee
Download 1a163c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 51 2018-12-05T13:14:21+01:00

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

Trying to find witnesses for program (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.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 '17

Trying to find witnesses for program (aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268, sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i, aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/aac994f94d4768ada65ed67ab31a9674240595ecec75018f92780c3f05cc7268.json

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