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-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i
programSHA 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
witnessName results-validated/cpa-seq-validate-violation-witnesses-smack.2018-12-08_2205.logfiles/sv-comp19_prop-memsafety.sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml
witnessSHA 26639ba205bb79dd8153a8a7708ba2922d0571eaf7104745f5f2f87443ff873d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T22:08:54+01:00
inputwitnesshash 18996e8d3e4c29af59d645010c509864f2169c6e455166d321e2969de580c872
producer CPAchecker 1.7-svn 29852
program-sha256 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
programfile ../../sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i
programhash 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memcleanup) )
witness-file witnessFileByHash/26639ba205bb79dd8153a8a7708ba2922d0571eaf7104745f5f2f87443ff873d.graphml
witness-sha256 26639ba205bb79dd8153a8a7708ba2922d0571eaf7104745f5f2f87443ff873d
witness-size 16655
witness-type correctness_witness

This witness was created for this program (cf. table above, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc).

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

Trying to find witnesses for program (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.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 (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.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 (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.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 (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.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 (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 16 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download db19c90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2019-12-01 11:52:35
Download fcf8f1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 19 2019-12-11T21:55:04+01:00 Download 07c42bd
Download 7efbeb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 18 2019-12-11T21:42:20+01:00 Download 343110e
Download c807883 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 20 2019-12-11T21:09:07+01:00 Download db19c90
Download e89246d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 19 2019-12-08T00:07:04+01:00 Download 76b8c19
Download 3544b54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 19 2019-12-07T21:16:49+01:00 Download 8d19418
Download 18605cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 18 2019-12-03T08:09:39+01:00 Download a8ba1da
Download a8ba1da Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 18 2019-11-30T08:16:08+01:00
Download 343110e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 18 2019-12-01T19:14:03+01:00
Download 6b702b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 12:55:52
Download 14fbb93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:40:41+01:00 Download 60c9b6a
Download ea80ff3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 20 2019-12-11T21:28:20+01:00 Download c34bac0
Download b99f484 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-07T21:18:30+01:00 Download 4454dbc
Download c34bac0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 20 2019-12-01T00:43:00+01:00
Download 20b4dbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-03T08:09:24+01:00 Download d0be55e
Download d0be55e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 16 2019-11-30T02:25:43+01:00

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

Trying to find witnesses for program (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 19 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 76f8edc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T06:34 CET (sv-comp)
Download 18996e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 6 2018-12-08T00:57:55
Download 66580ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-08T23:44:25+01:00 Download 76f8edc
Download e18bacc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 19 2018-12-07T09:12:57+01:00 Download a8f9cde
Download 70d9b93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-06T10:19:27+01:00 Download cfdfdbf
Download be73682 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-06T09:47:59+01:00 Download 46ea4fa
Download 46ea4fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-05T22:32:43+01:00
Download 26639ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-08T22:08:54+01:00 Download 18996e8
Download d275db4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T16:12 CET (sv-comp)
Download 8b50e09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 6 2018-12-08T12:08:41
Download 37411c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 25 2018-12-07T00:25 CET (sv-comp)
Download 23c4762 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 20 2018-12-07T06:29:54+01:00
Download 5a2bc6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:53:08+01:00 Download fe2c802
Download ba0892f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:37:14+01:00 Download ecc899e
Download a82921c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:28:59+01:00 Download 12640dd
Download 3310b6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-08T08:54:45+01:00 Download 23c4762
Download ffe3f52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-06T09:12:01+01:00 Download 9da34e9
Download ae216c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:48:51+01:00 Download 54b3882
Download 54b3882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-06T06:53:07+01:00

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

Trying to find witnesses for program (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.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 (6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc, sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i, 6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6798ac5dbb1e16ae2d611aa8c0a82d88dce24a5b074dbd97c1ae1826e80111cc.json

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