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/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programSHA fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
witnessName results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml
witnessSHA d0c58c32db8be91b4bdf8a4696f11c5f3f7c501891d19676eb7a83c00874f3c3

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T16:50 CET (sv-comp)
producer CBMC
program-sha256 fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programhash d5f013930ebf37bbb37b715f6518f407edf26521
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/d0c58c32db8be91b4bdf8a4696f11c5f3f7c501891d19676eb7a83c00874f3c3.graphml
witness-sha256 d0c58c32db8be91b4bdf8a4696f11c5f3f7c501891d19676eb7a83c00874f3c3
witness-size 71250
witness-type violation_witness

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

Trying to find witnesses for program (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.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 (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.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 (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.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 (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.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 (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.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 '19

Trying to find witnesses for program (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eeab5c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 12 2018-12-08T07:37 CET (sv-comp)
Download 40119a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 27 2018-12-08T12:29:53
Download e13aa4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 93 2018-12-06T21:17:02+01:00
Download 88a0c71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 92 2018-12-09T20:19:34+01:00 Download f83af19
Download e91e585 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 95 2018-12-09T17:46:58+01:00 Download 28ed974
Download 9353a44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 94 2018-12-08T23:43:55+01:00 Download eeab5c7
Download bd92947 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 92 2018-12-08T08:38:43+01:00 Download e13aa4c
Download f031f3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 92 2018-12-06T09:47:57+01:00 Download 6ec2d34
Download 6ec2d34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 97 2018-12-05T20:06:18+01:00
Download 1816867 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 57 2018-12-10T20:34:53+01:00 Download 75f3c3c
Download ab40c24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 57 2018-12-08T22:08:43+01:00 Download 40119a6
Download 34d0b72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 57 2018-12-08T04:54:45+01:00 Download 99adb07
Download 848a9d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 57 2018-12-06T10:16:25+01:00 Download bedc8e1
Download 1e5ccf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 57 2018-12-06T09:42:51+01:00 Download 7bac66e
Download d2af17c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 57 2018-12-06T09:19:39+01:00 Download c5fb43d

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

Trying to find witnesses for program (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 12 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e8cdc7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 69 Sat Dec 2 19:40:45 2017
Download 7c82438 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 11 2017-12-02T14:47 CET (sv-comp)
Download 4d1f8c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 116 2017-12-02T14:34Z
Download 21d058e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 16 2017-12-01T23:12:43.874489
Download 0573cf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 17 2017-12-01T08:23:17.519852
Download 62a6d32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 35 2017-11-30T16:13 CET (sv-comp)
Download 6f9bd68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 93 2017-11-30T21:57:37+01:00
Download a06bf01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 133 2017-11-30T22:28:11+01:00
Download ef596c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 57 2017-12-01T03:29:08+01:00
Download 71e6540 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 55 2017-12-01T22:59:55+01:00
Download d0c58c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 71 2017-11-30T16:50 CET (sv-comp)
Download 1dedec0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 54 2017-11-30T18:56 CET (sv-comp)

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

Trying to find witnesses for program (fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/fc662187ab96b0d7e69d745dd32dc35071a960bf83dee85d84ec82f3e88a801a.json

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