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_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c
programSHA b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
witnessName results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c.files/witness.graphml
witnessSHA d02c3b5c585c3ff5c8bb1cf1ce64ec369729da1b8190f03b9dda8b6fa0a17a73

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T17:48:32+01:00
producer CPAchecker 1.6.1-svn 26725
program-sha256 b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c
programhash b3b24d22acbd30abb2bd6c739c1741063240b31f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/d02c3b5c585c3ff5c8bb1cf1ce64ec369729da1b8190f03b9dda8b6fa0a17a73.graphml
witness-sha256 d02c3b5c585c3ff5c8bb1cf1ce64ec369729da1b8190f03b9dda8b6fa0a17a73
witness-size 39190
witness-type violation_witness

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

Trying to find witnesses for program (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.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 (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.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 (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.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 (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.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 (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d63bf3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 5 2019-12-01 16:21:48
Download 6fed6e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 61 2019-12-03T23:25 CET (comp)
Download a4db661 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 76 2019-12-11T21:39:43+01:00 Download 2b41fe0
Download 4c733c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 76 2019-12-11T20:55:21+01:00 Download dec8861
Download 52a6e94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 76 2019-12-11T20:44:39+01:00 Download 5cd3266
Download 554d202 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 76 2019-12-08T01:52:11+01:00 Download 8115bb4
Download 3e3cbc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 79 2019-12-08T00:26:03+01:00 Download 0ac8f70
Download a3f8ea2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 79 2019-12-07T21:13:16+01:00 Download b946a94
Download 3c4bb89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 76 2019-12-03T08:10:18+01:00 Download 8ebf756
Download 8ebf756 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 70 2019-11-30T01:24:26+01:00
Download 8115bb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 57 2019-12-07T15:20:43+01:00
Download 2b41fe0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 75 2019-11-30T21:17:41+01:00
Download 0e3ad4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 83 2019-12-11T21:09:40+01:00 Download d63bf3f
Download bf4f90f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 83 2019-12-05T20:20:51+01:00 Download 3d04c17
Download 76f5783 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 83 2019-12-05T19:34:01+01:00 Download a162201
Download e320aa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 83 2019-12-04T02:58:21+01:00 Download 6fed6e0

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

Trying to find witnesses for program (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 17 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bb42810 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T13:20 CET (sv-comp)
Download 46c88ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 28 2018-12-08T04:07:51
Download 51579e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 76 2018-12-07T01:16:46+01:00
Download 31e73bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 79 2018-12-09T20:53:08+01:00 Download d42c03e
Download 65ba964 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 79 2018-12-09T20:37:38+01:00 Download 1378633
Download b2c4227 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-09T18:21:07+01:00 Download b0d05c0
Download a7ec9d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-08T23:42:21+01:00 Download bb42810
Download 9270877 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-08T08:56:24+01:00 Download 51579e1
Download 1aa6e52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-08T05:02:11+01:00 Download 00cc729
Download 02f405e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-08T04:19:06+01:00 Download 3621a75
Download 8b52ff5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-06T10:18:36+01:00 Download 06db584
Download 28dce4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-06T09:48:12+01:00 Download cad9534
Download cad9534 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 70 2018-12-06T06:57:37+01:00
Download f020c1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-10T20:36:20+01:00 Download e529e1f
Download f2b9940 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-08T22:09:42+01:00 Download 46c88ff
Download 43c64b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-06T09:40:39+01:00 Download 33ecbff
Download e909e83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-06T09:09:34+01:00 Download 98e50bb

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

Trying to find witnesses for program (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4424167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 59 Sun Dec 3 01:36:34 2017
Download e9c6207 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 112 2017-12-03T02:39Z
Download 1c24e15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 6 2017-12-02T07:56 CET (sv-comp)
Download b5e6f63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 13 2017-12-02T04:51:27.746645
Download 7756865 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 10 2017-12-01T18:27:44.786508
Download b1b67df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 41 2017-11-30T18:19 CET (sv-comp)
Download 3adb778 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 70 2017-11-30T15:32:10+01:00
Download ee956a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 130 2017-11-30T23:37:22+01:00
Download d02c3b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 39 2017-11-30T17:48:32+01:00
Download 30f9506 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 41 2017-12-02T13:43:56+01:00
Download 472fbf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 63 2017-11-30T23:48 CET (sv-comp)
Download 156a75e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 112 2017-12-02T07:24Z
Download cfddd32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 64 2017-12-01T01:46 CET (sv-comp)

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

Trying to find witnesses for program (b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json

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