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_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programSHA 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
witnessName results-verified/uautomizer.2018-12-08_0742.logfiles/sv-comp19_prop-reachsafety.pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml
witnessSHA 017ed8a095db724f962751dd3549d29c5779e120c7988ecd29c41d6b0f89c42d

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/017ed8a095db724f962751dd3549d29c5779e120c7988ecd29c41d6b0f89c42d.json

Key Value
architecture 32bit
creationtime 2018-12-08T23:23Z
producer Automizer
programfile /tmp/vcloud-vcloud-master/worker/working_dir_7ee9fa25-a73d-435a-9c4c-6f68aef3df0f/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programhash 077fe0fcd97be15aa2e10e89ce167f8b22d1af7e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/017ed8a095db724f962751dd3549d29c5779e120c7988ecd29c41d6b0f89c42d.graphml
witness-sha256 017ed8a095db724f962751dd3549d29c5779e120c7988ecd29c41d6b0f89c42d
witness-size 424746
witness-type violation_witness

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

Trying to find witnesses for program (20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 484e994 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 451 2019-12-11T22:00:30+01:00 Download 67a9c41
Download 1226ef4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 259 2019-12-11T20:44:57+01:00 Download 74a19f9
Download dccc2dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 210 2019-12-08T01:51:38+01:00 Download b18a455
Download fe95024 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 208 2019-12-03T08:10:27+01:00 Download 39b68e5
Download 39b68e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 217 2019-11-30T03:37:23+01:00
Download b18a455 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 193 2019-12-07T15:55:07+01:00
Download 67a9c41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 452 2019-12-01T08:41:58+01:00
Download 1359633 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 73 2019-12-11T21:09:30+01:00 Download 95bd17d
Download bfae424 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 73 2019-12-11T20:54:52+01:00 Download 615c0fe
Download c5365d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 73 2019-12-07T21:12:38+01:00 Download 6f654f9
Download 03a8346 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 73 2019-12-05T20:21:54+01:00 Download a484bda
Download dd4ddc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 73 2019-12-05T19:34:14+01:00 Download 85ffe16
Download 0fabe75 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 5 2019-12-01 11:04:35

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

Trying to find witnesses for program (20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4432034 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 9 2018-12-08T14:27 CET (sv-comp)
Download 9ef5f9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 33 2018-12-08T14:30:35
Download f7fd60d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 460 2018-12-08T04:05:37+01:00
Download 6d7eb23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-09T18:20:20+01:00 Download 30c53cb
Download 3c7443c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 209 2018-12-08T23:42:05+01:00 Download 4432034
Download 0753814 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 451 2018-12-08T08:36:01+01:00 Download f7fd60d
Download 96d321f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 208 2018-12-06T09:48:19+01:00 Download c002623
Download c002623 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 217 2018-12-05T11:17:04+01:00
Download 1778f7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 73 2018-12-10T20:38:23+01:00 Download 3364d19
Download 0ee5e7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-09T20:37:49+01:00 Download 017ed8a
Download 3f64190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 73 2018-12-08T22:10:28+01:00 Download 9ef5f9c
Download f818dc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 73 2018-12-08T05:02:24+01:00 Download 904dcee
Download 772502b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 73 2018-12-06T10:18:58+01:00 Download 298f33c
Download 2e67089 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 73 2018-12-06T09:42:15+01:00 Download 0d6698d
Download d83e0a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 73 2018-12-06T09:14:53+01:00 Download 3ca64dd

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

Trying to find witnesses for program (20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 10 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 83afcf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 177 Sat Dec 2 21:57:43 2017
Download 4d89e4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 3 2017-12-02T01:00 CET (sv-comp)
Download 39a1752 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 26 2017-12-02T05:17:58.082558
Download 53866b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 18 2017-12-01T08:25:53.964759
Download 592fdfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 69 2017-12-01T07:11 CET (sv-comp)
Download 739a81e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 209 2017-11-30T22:30:02+01:00
Download e8407fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 291 2017-12-01T00:34:25+01:00
Download fda71e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 261 2017-11-30T12:58 CET (sv-comp)
Download 65853a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 243 2017-12-02T11:50Z
Download 08c3e0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 91 2017-12-01T02:33 CET (sv-comp)

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

Trying to find witnesses for program (20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

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

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