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-rb-sentinel_false-unreach-call_false-valid-memcleanup.i
programSHA 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
witnessName results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml
witnessSHA 0354ac26a30514f74f256d4569fbe54361979d81418dfafec149d75188020528

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/0354ac26a30514f74f256d4569fbe54361979d81418dfafec149d75188020528.json

Key Value
architecture 32bit
creationtime 2017-12-01T20:40 CET (sv-comp)
producer Map2Check
program-sha256 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
programfile ../../sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i
programhash d9f9c3b0fdd5428a38e0eab9236fadbdbb3aa880
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0354ac26a30514f74f256d4569fbe54361979d81418dfafec149d75188020528.graphml
witness-sha256 0354ac26a30514f74f256d4569fbe54361979d81418dfafec149d75188020528
witness-size 2922
witness-type violation_witness

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

Trying to find witnesses for program (913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751, sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a0f15ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2019-12-02 04:11:45
Download 67aa82c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 10 2019-12-11T21:50:26+01:00 Download 65a3f79
Download e2d7dbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 12 2019-12-11T21:09:03+01:00 Download a0f15ba
Download 2d1f0b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 13 2019-12-08T00:07:37+01:00 Download 7f42477
Download 7329ae9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 10 2019-12-07T21:14:50+01:00 Download 6fa8401
Download cac0195 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 10 2019-12-03T08:09:42+01:00 Download 79aeec1
Download 79aeec1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 10 2019-11-30T14:09:22+01:00
Download 65a3f79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 10 2019-11-30T20:55:45+01:00
Download 87c48a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 18:13:48
Download 4638e5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T21:47:33+01:00 Download 0e42b1b
Download 0921d86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T21:45:39+01:00 Download 8126286
Download c4595db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-08T00:06:02+01:00 Download 4e6947b
Download 395d8fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-07T21:17:22+01:00 Download cc4c869
Download da7a8ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-03T08:57:31+01:00 Download b4a19e2
Download cfda812 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-03T08:10:02+01:00 Download e01464a
Download e01464a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 16 2019-11-30T01:42:12+01:00
Download b90aa70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 7 2019-12-07T14:41:18+01:00
Download 8126286 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 16 2019-11-30T21:27:24+01:00
Download d12ef21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T21:09:18+01:00 Download 87c48a5
Download ceb9c38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T20:45:54+01:00 Download 9eb58fd
Download d32cfd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-08T01:51:19+01:00 Download b90aa70
Download 868fa26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-05T20:21:48+01:00 Download 5f2edce

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

Trying to find witnesses for program (913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751, sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e7c519b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T07:35 CET (sv-comp)
Download 42a56a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 3 2018-12-08T10:25:12
Download cbcdc34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T23:44:42+01:00 Download e7c519b
Download 3b1604a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T22:09:47+01:00 Download 42a56a4
Download 68fb635 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-07T09:14:58+01:00 Download 8a77f61
Download 05af135 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T10:17:20+01:00 Download 8316090
Download ffbbd93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:48:20+01:00 Download dc1a4d3
Download dc1a4d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-05T13:41:08+01:00
Download 3406397 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:20:13+01:00 Download 334a77b
Download 525739b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T04:07 CET (sv-comp)
Download 39f4e30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T11:45:21
Download 0cf7c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 7 2018-12-10T18:14:40+01:00
Download c6036a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 16 2018-12-07T11:00:48+01:00
Download 3497672 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-10T10:48:53+01:00 Download fc79e00
Download a6180cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T20:39:37+01:00 Download a131153
Download 16aad16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T20:26:04+01:00 Download b32293e
Download 5f7f9c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T22:07:32+01:00 Download 39f4e30
Download 0f12999 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T08:17:56+01:00 Download c6036a0
Download 93a5f79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T04:59:00+01:00 Download 5c65b81
Download 0428ef4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T03:44:12+01:00 Download fc79e00
Download 5aa566e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-07T09:28:26+01:00 Download e23eab4
Download b4ef143 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T10:18:31+01:00 Download ab9f9db
Download 455f96f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:48:47+01:00 Download 503d449
Download 03ae420 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:19:39+01:00 Download 2107cbb
Download 503d449 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T01:44:09+01:00
Download 48345d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-10T20:35:00+01:00 Download 0cf7c9d
Download 267f743 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T18:23:08+01:00 Download ad9f391
Download 3ef4984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T23:43:10+01:00 Download 525739b
Download 1202b85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-07T01:09:31+01:00 Download cc9f011

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

Trying to find witnesses for program (913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751, sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i).

Found 13 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cecb261 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T06:02 CET (sv-comp)
Download e23eab4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 5 2017-12-01T20:24 CET (sv-comp)
Download 0354ac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T20:40 CET (sv-comp)
Download 27c6e0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 14 2017-12-02T08:25Z
Download ede7017 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 8 2017-12-01T17:47 CET (sv-comp)
Download 536e4e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 6 2017-12-01T22:26:54.017662
Download 64f2648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 6 2017-12-01T17:32:11.437240
Download b3d2ac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T04:37 CET (sv-comp)
Download 13d9fa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 14 2017-12-01T01:04:23+01:00
Download 17f720d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 23 2017-11-30T13:34:09+01:00
Download a6d6689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T02:39:19+01:00
Download 991371d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 12 2017-11-30T17:45 CET (sv-comp)
Download cfe9433 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 14 2017-12-02T13:41Z

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

Trying to find witnesses for program (913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751, sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i).

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

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