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/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i
programSHA 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-memsafety.sll2n_append_equal_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA f3d67d86ec531e9b3e1312d1c47a75ab189708cd739f5f963b9cdfdf2c18c9bd

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T08:12:54.449985
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i
programhash 1c66d86f2cb93b92fe110cb1d9c29158a00f0747
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/f3d67d86ec531e9b3e1312d1c47a75ab189708cd739f5f963b9cdfdf2c18c9bd.graphml
witness-sha256 f3d67d86ec531e9b3e1312d1c47a75ab189708cd739f5f963b9cdfdf2c18c9bd
witness-size 3436
witness-type correctness_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 90deaa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 12 2019-11-30T07:41:56+01:00
Download 96f2cb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 12 2019-11-30T23:37:47+01:00
Download d34a505 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:37 CET (comp)
Download fa926f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-11T20:38:47+01:00 Download 7b216a9
Download 7d81ca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-11T20:35:00+01:00 Download ddb99d0
Download 1ae949e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-11T20:17:35+01:00 Download 26cce8d
Download dfe09be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-08T01:09:23+01:00 Download 1584efa
Download d2a94a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-08T00:02:30+01:00 Download 38196a3
Download b134d3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-07T19:54:33+01:00 Download b93233c
Download 90d1dcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-06T02:26:54+01:00 Download a063088
Download 16e2b45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-05T19:27:54+01:00 Download b68f5af
Download 849c06d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-04T02:22:12+01:00 Download d34a505
Download d5767f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-11-30T20:12:18+01:00 Download 1f2bd46
Download 5d577ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-11-30T17:14:32+01:00 Download f9a43d6
Download f9a43d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 37 2019-11-30T03:10:32+01:00
Download 1584efa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 14 2019-12-07T22:22:09+01:00
Download ddb99d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 13 2019-11-30T23:26:37+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 55edfe4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T04:22 CET (sv-comp)
Download 91921e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 12 2018-12-07T06:50:48+01:00
Download 26fb706 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-05T14:49:46+01:00
Download 7f554f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T05:39 CET (sv-comp)
Download 50ec26b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:33:39
Download 2288eb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T20:48 CET (sv-comp)
Download e923005 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 14 2018-12-10T17:30:49+01:00
Download 48fb01f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 41 2018-12-06T20:08:26+01:00
Download b25c13a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T20:02:49+01:00 Download e923005
Download dd2bfab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-10T10:31:43+01:00 Download 9e71dbf
Download 96a8008 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T23:12:50+01:00 Download 7f554f8
Download e1b2a3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T21:48:08+01:00 Download 50ec26b
Download 7c98530 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T06:16:11+01:00 Download 48fb01f
Download f82edc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T02:50:49+01:00 Download 9a86e8d
Download 2a04380 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T01:48:38+01:00 Download 9e71dbf
Download 65f0515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-07T16:38:10+01:00 Download 2288eb9
Download 011c67e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-07T08:53:03+01:00 Download 602ae39
Download 8c28fb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T09:28:50+01:00 Download ff2b28a
Download 4e3959e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:57:34+01:00 Download 1edc38f
Download 007258b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:04:51+01:00 Download ab2414a
Download 33734a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:02:25+01:00 Download d737317
Download 1edc38f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 42 2018-12-05T21:20:41+01:00

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

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

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

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

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