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.4_1.ufo.UNBOUNDED.pals.c
programSHA 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34
witnessName results-validated/cpa-seq-validate-violation-witnesses-verifuzz.2018-12-09_1743.logfiles/sv-comp19_prop-reachsafety.pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c.files/witness.graphml
witnessSHA 934512d46db4d22e7f4e72d1e9c311e4de1da490fbc504a5e457a4538480375e

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/934512d46db4d22e7f4e72d1e9c311e4de1da490fbc504a5e457a4538480375e.json

Key Value
architecture 32bit
creationtime 2018-12-09T18:20:38+01:00
inputwitnesshash 1f22531aa58ec3348a255bc215e8f4b98f0e920a8352cfe0783e5547bf69dcf9
producer CPAchecker 1.7-svn 29852
program-sha256 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c
programhash 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/934512d46db4d22e7f4e72d1e9c311e4de1da490fbc504a5e457a4538480375e.graphml
witness-sha256 934512d46db4d22e7f4e72d1e9c311e4de1da490fbc504a5e457a4538480375e
witness-size 467643
witness-type violation_witness

This witness was created for this program (cf. table above, 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34).

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

Trying to find witnesses for program (648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c).

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

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

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

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

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c, 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8c303ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 102 2019-12-03T22:38 CET (comp)
Download 6d72342 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 130 2019-12-11T21:45:03+01:00 Download 34e48fe
Download 271941d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 271 2019-12-11T20:44:38+01:00 Download 7043976
Download fab7f06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 133 2019-12-08T01:51:26+01:00 Download 0adf12c
Download 6f4a853 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 133 2019-12-08T00:27:18+01:00 Download 082f982
Download c9d18fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 133 2019-12-07T21:16:18+01:00 Download 99a4a41
Download e4760c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 133 2019-12-03T08:09:11+01:00 Download ffb8a94
Download ffb8a94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 139 2019-11-30T08:21:32+01:00
Download 0adf12c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 99 2019-12-07T14:08:26+01:00
Download 34e48fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 130 2019-12-01T07:02:39+01:00
Download 4df52f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 81 2019-12-11T21:09:48+01:00 Download c04a3b8
Download 87c402d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-11T20:54:37+01:00 Download 62217fb
Download a719906 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-05T20:20:27+01:00 Download 42d8bad
Download 36bb790 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-05T19:34:13+01:00 Download bb8e67a
Download 8411357 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-04T02:58:13+01:00 Download 8c303ce
Download 6f885f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 02:41:00

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

Trying to find witnesses for program (648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c).

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c, 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 31699fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T05:02 CET (sv-comp)
Download e743ac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 42 2018-12-08T12:13:01
Download 24ad991 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 131 2018-12-07T22:58:57+01:00
Download 934512d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 468 2018-12-09T18:20:38+01:00 Download 1f22531
Download a15cf08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 132 2018-12-08T23:44:52+01:00 Download 31699fb
Download 878da0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 131 2018-12-08T08:59:01+01:00 Download 24ad991
Download 8022645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 133 2018-12-06T09:48:23+01:00 Download b984012
Download b984012 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 139 2018-12-06T04:42:14+01:00
Download ebadd10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-10T20:35:34+01:00 Download 216ed89
Download 6a4a30e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-09T20:53:31+01:00 Download 796c0d2
Download 67140bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-09T20:40:08+01:00 Download 77cf060
Download c2e21e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-08T22:09:24+01:00 Download e743ac9
Download 5e64a0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-08T04:54:47+01:00 Download fa90ba5
Download f1b80b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-06T10:20:04+01:00 Download b109723
Download 190a177 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-06T09:41:56+01:00 Download b3b8e45
Download f4768f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-06T09:19:27+01:00 Download 40d35c5

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

Trying to find witnesses for program (648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c).

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c, 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 168455d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 99 Sat Dec 2 17:42:39 2017
Download c5e0b9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 181 2017-12-02T20:37Z
Download 7e871d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 6 2017-12-01T23:15 CET (sv-comp)
Download e1f7405 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 18 2017-12-01T14:56:57.801438
Download 9fdc434 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 22 2017-12-01T20:39:57.000223
Download ba507a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 62 2017-12-01T02:47 CET (sv-comp)
Download e68ffe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 135 2017-12-01T00:25:50+01:00
Download f38f68d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 207 2017-11-30T22:24:26+01:00
Download 0c37df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 64 2017-11-30T23:48:02+01:00
Download b066840 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 68 2017-12-02T10:36:31+01:00
Download 6302ef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 101 2017-12-01T02:28 CET (sv-comp)
Download 76489b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 181 2017-12-02T11:19Z
Download 10b5ee7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 108 2017-11-30T18:21 CET (sv-comp)

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

Trying to find witnesses for program (648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c, 648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/648b4c1d6e1f11bfe2b84e822d1b39edf160b0c101f2d55835b1ffa946421b34.json

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