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/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i
programSHA 8807e938b59ca37b0c40db90c0f7cd7e3795306066f5090ea6a090a43216d296
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-memsafety.sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA 15709fb25dd4d7d94037b20d40d25be30bab274eb1902b1d71e720da6e237ca7

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T13:19:58+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 8807e938b59ca37b0c40db90c0f7cd7e3795306066f5090ea6a090a43216d296
programfile ../../sv-benchmarks/c/list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i
programhash 8807e938b59ca37b0c40db90c0f7cd7e3795306066f5090ea6a090a43216d296
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free) )
witness-file witnessFileByHash/15709fb25dd4d7d94037b20d40d25be30bab274eb1902b1d71e720da6e237ca7.graphml
witness-sha256 15709fb25dd4d7d94037b20d40d25be30bab274eb1902b1d71e720da6e237ca7
witness-size 15921
witness-type correctness_witness

This witness was created for this program (cf. table above, 8807e938b59ca37b0c40db90c0f7cd7e3795306066f5090ea6a090a43216d296).

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cbbefd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 16 2019-12-01T14:45:56+01:00
Download a31271b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 16 2019-11-29T15:03:10+01:00
Download afc44bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:00 CET (comp)
Download ff1c430 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:54:20+01:00 Download f16a736
Download 06edab0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:30:21+01:00 Download 4950340
Download bfb1b2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:17:04+01:00 Download 41212ed
Download 922152e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-08T01:16:39+01:00 Download 178fc9b
Download 3221f0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-08T00:00:28+01:00 Download 9bf633b
Download f785e1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-07T20:01:34+01:00 Download 53b51a7
Download 6184d44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-06T02:09:41+01:00 Download e3f6504
Download 0972b13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-05T19:27:30+01:00 Download 9e57ca1
Download 8fa34b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-04T02:22:32+01:00 Download afc44bb
Download 885a5e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-11-30T19:21:18+01:00 Download d8e2fc4
Download d6e47ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-11-30T17:38:32+01:00 Download 47f90a8
Download 47f90a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 20 2019-11-30T14:49:43+01:00
Download 178fc9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 18 2019-12-07T14:30:48+01:00
Download f16a736 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 16 2019-12-01T19:39:40+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 98dcd56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T02:09 CET (sv-comp)
Download 4943091 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-05T21:19:04+01:00
Download 15709fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 16 2018-12-06T13:19:58+01:00
Download 76f16ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T12:01 CET (sv-comp)
Download 15830bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T12:56:54
Download 637e522 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:04 CET (sv-comp)
Download 1dcd6ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 18 2018-12-10T19:18:48+01:00
Download 33a16cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 20 2018-12-07T19:37:56+01:00
Download 9a92a65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-10T20:04:54+01:00 Download 1dcd6ad
Download a1ff8b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-10T10:31:20+01:00 Download 18e70da
Download 6a78bfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T23:13:35+01:00 Download 76f16ed
Download d108c57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T21:29:36+01:00 Download 15830bd
Download e8c0d16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T07:10:58+01:00 Download 33a16cb
Download 52429e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T02:27:51+01:00 Download 7a7964c
Download 9a4ad58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T02:08:53+01:00 Download 18e70da
Download e36a44c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-07T16:39:39+01:00 Download 637e522
Download a1b782a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-07T08:52:49+01:00 Download 978bff6
Download 3cb7791 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:28:31+01:00 Download e0d3de1
Download 87f7c06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T08:55:22+01:00 Download 6eb58da
Download ba4f8bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T08:10:55+01:00 Download e1550a9
Download 4219dc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T08:06:37+01:00 Download 446ab1b
Download 6eb58da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-05T22:48:41+01:00

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

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

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

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

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