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 (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

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

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

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

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

Found 11 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7d1c267 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 181 2019-12-03T22:54 CET (comp)
Download 549b206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 274 2019-12-11T21:59:22+01:00 Download 969a8e5
Download 4680084 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 258 2019-12-11T20:44:27+01:00 Download a2c97f2
Download 4621a74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 274 2019-12-03T08:10:32+01:00 Download 06041c0
Download 06041c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 281 2019-11-29T14:45:12+01:00
Download 969a8e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 276 2019-12-01T01:57:05+01:00
Download 7471712 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 52 2019-12-11T20:55:21+01:00 Download c98ceb5
Download 1209151 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 52 2019-12-08T01:52:18+01:00 Download fc1b193
Download 0bbc75d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 51 2019-12-05T20:21:07+01:00 Download 98e2c19
Download 12f32b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 52 2019-12-05T19:34:57+01:00 Download 3549874
Download f5abc00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 53 2019-12-04T02:58:30+01:00 Download 7d1c267

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

Trying to find witnesses for program (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c15f538 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 12 2018-12-08T03:11 CET (sv-comp)
Download d4ebf95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 65 2018-12-08T06:27:11
Download 774f578 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 278 2018-12-06T23:55:05+01:00
Download 8e51c6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 258 2018-12-09T18:21:07+01:00 Download 56888c5
Download 17be90a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 258 2018-12-08T23:43:30+01:00 Download c15f538
Download 9b9e160 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 275 2018-12-08T08:28:19+01:00 Download 774f578
Download 6b70ae8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 275 2018-12-06T09:48:28+01:00 Download 10b88fd
Download 10b88fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 281 2018-12-06T00:50:27+01:00
Download 9f655d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 52 2018-12-10T20:37:02+01:00 Download c4ff9c3
Download d90a4c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 52 2018-12-08T22:10:31+01:00 Download d4ebf95
Download e386687 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 52 2018-12-08T05:06:08+01:00 Download 84063be
Download 97474c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 52 2018-12-06T10:20:14+01:00 Download b91e134
Download 802746f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 52 2018-12-06T09:42:49+01:00 Download fac6b34
Download da173b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 51 2018-12-06T09:09:52+01:00 Download 6846948

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

Trying to find witnesses for program (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 8 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 931b1d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 194 Sat Dec 2 21:27:44 2017
Download bd68ed1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 12 2017-12-02T03:23 CET (sv-comp)
Download e66c047 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 31 2017-12-02T01:58:51.946594
Download f513927 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 32 2017-12-01T10:39:50.639902
Download 1c12155 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 86 2017-11-30T16:44 CET (sv-comp)
Download cdc0e78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 271 2017-11-30T17:46:49+01:00
Download fe8ba75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 199 2017-11-30T17:26 CET (sv-comp)
Download e4ec2e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 168 2017-12-01T01:29 CET (sv-comp)

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

Trying to find witnesses for program (1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1a670b4fbeabf1f11baa9f4cc2bb55de60afce7eda87c258973d4f43d63c6636.json

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