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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.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 (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.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 (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.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 (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.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 (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b7bc4a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 4 2019-12-01 08:27:28
Download 355e194 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 81 2019-12-04T00:59 CET (comp)
Download a9bb10d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 122 2019-12-11T21:57:15+01:00 Download f8230d6
Download 06596d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 118 2019-12-11T21:40:27+01:00 Download 6fdca59
Download fc76d8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 114 2019-12-11T21:09:06+01:00 Download b7bc4a1
Download 91dc839 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 114 2019-12-11T20:44:32+01:00 Download 15c9990
Download 26abaf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 115 2019-12-07T21:18:39+01:00 Download e8f08fd
Download 579a2c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 121 2019-12-03T08:57:12+01:00 Download 3243c28
Download 88551e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 118 2019-12-03T08:10:29+01:00 Download 2153264
Download 2153264 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 120 2019-11-30T07:28:25+01:00
Download 6fdca59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 118 2019-12-01T08:08:47+01:00
Download 9788e90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 32 2019-12-11T20:54:53+01:00 Download 62afab7
Download e0b987e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 33 2019-12-08T01:51:19+01:00 Download 7975215
Download 5c18289 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 32 2019-12-05T20:20:49+01:00 Download 01d71c3
Download 0282fc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 33 2019-12-05T19:34:13+01:00 Download 6e5bf78
Download 6dd92bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 32 2019-12-04T02:58:25+01:00 Download 355e194
Download 2fb07ce Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 14:20:38
Download 80341d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:39 CET (comp)

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

Trying to find witnesses for program (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d34bd99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T16:05 CET (sv-comp)
Download 9821c6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 30 2018-12-08T12:02:48
Download bedf00c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 119 2018-12-07T00:09:37+01:00
Download 3e61050 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 115 2018-12-09T20:19:21+01:00 Download 6a1adbc
Download ef83785 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 114 2018-12-09T18:00:23+01:00 Download 5a42474
Download 01ad731 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 114 2018-12-08T23:43:46+01:00 Download d34bd99
Download 2b70de3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 118 2018-12-08T08:03:21+01:00 Download bedf00c
Download f00d153 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 121 2018-12-08T04:26:56+01:00 Download 0235b3b
Download c3b3b67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 118 2018-12-06T09:48:26+01:00 Download 51c553c
Download 51c553c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 120 2018-12-06T05:28:32+01:00
Download 0d265d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-10T20:38:13+01:00 Download 8d4e4cb
Download be5de8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 32 2018-12-08T22:09:14+01:00 Download 9821c6e
Download a81cf71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-08T05:01:27+01:00 Download 6f6d641
Download 7589da9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-06T10:18:18+01:00 Download 7e3df7e
Download eb4baf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-06T09:42:42+01:00 Download 373a649
Download f392e38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 32 2018-12-06T09:12:26+01:00 Download c6320ab
Download f31252a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T02:51 CET (sv-comp)
Download 358fb46 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T08:42 CET (sv-comp)

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

Trying to find witnesses for program (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7d42091 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 87 Sat Dec 2 20:56:04 2017
Download f663f64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2017-12-02T18:53 CET (sv-comp)
Download 457d6bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 16 2017-12-01T17:49:18.688877
Download e3c2d57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 16 2017-12-01T16:18:38.142043
Download 957e2ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 41 2017-12-01T16:35 CET (sv-comp)
Download c45f4be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 39 2017-12-01T02:03 CET (sv-comp)
Download 006094e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 117 2017-11-30T19:18:38+01:00
Download 206de52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 75 2017-12-02T03:30:57+01:00
Download 5f87235 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 76 2017-11-30T16:22 CET (sv-comp)
Download e51abfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:10:39.309795
Download 835af46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:24:02.640796
Download 290a892 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 160 2017-12-01T17:53 CET (sv-comp)
Download 38783ca Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 62 2017-12-01T13:34 CET (sv-comp)

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

Trying to find witnesses for program (71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json

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