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 (d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.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.1.ufo.BOUNDED-6.pals_true-termination.c, d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba.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 (d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.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.1.ufo.BOUNDED-6.pals_true-termination.c, d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba.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 (d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.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.1.ufo.BOUNDED-6.pals_true-termination.c, d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba.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 (d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.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.1.ufo.BOUNDED-6.pals_true-termination.c, d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba.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 (d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 978cac7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 4 2019-12-01 19:51:28
Download 4e6935e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 87 2019-12-03T22:50 CET (comp)
Download 1f71b1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 127 2019-12-11T21:40:27+01:00 Download a74c717
Download 801fca9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 127 2019-12-11T21:09:17+01:00 Download 978cac7
Download e500195 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 127 2019-12-11T20:44:41+01:00 Download 4930213
Download aecf021 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 129 2019-12-08T01:52:33+01:00 Download 2789643
Download e7d52e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 130 2019-12-03T08:56:55+01:00 Download 0caff69
Download 996803a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 129 2019-12-03T08:10:11+01:00 Download 0ab05c6
Download 0ab05c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 132 2019-11-29T15:18:59+01:00
Download 2789643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 108 2019-12-07T10:19:56+01:00
Download a74c717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 127 2019-12-01T01:36:33+01:00
Download c6c9284 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-11T20:55:24+01:00 Download d4a984b
Download efb81fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-05T20:21:20+01:00 Download e086795
Download f0fb16f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-05T19:34:17+01:00 Download 7ebd347
Download 12a1fa9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-04T02:58:19+01:00 Download 4e6935e
Download 8d55527 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 23:43:12
Download 6fc02ed Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:46 CET (comp)

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

Trying to find witnesses for program (d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.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.1.ufo.BOUNDED-6.pals_true-termination.c, d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1dba552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T15:30 CET (sv-comp)
Download e1ae8ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 33 2018-12-08T05:11:59
Download 365ffb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 128 2018-12-07T10:02:08+01:00
Download 2396a0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 129 2018-12-09T20:30:18+01:00 Download a52de6e
Download 946f945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 127 2018-12-09T17:49:26+01:00 Download add957c
Download 2accdaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 127 2018-12-08T23:44:04+01:00 Download 1dba552
Download db8fc96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 127 2018-12-08T08:55:21+01:00 Download 365ffb9
Download bb878f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 130 2018-12-08T03:44:37+01:00 Download ab66bbf
Download cac44d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 129 2018-12-06T09:49:00+01:00 Download 5268881
Download 5268881 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 132 2018-12-06T00:30:00+01:00
Download dcbce1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-10T20:36:12+01:00 Download 9d3c8b4
Download ad5a9c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-08T22:11:27+01:00 Download e1ae8ad
Download 1a34345 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-08T05:02:30+01:00 Download b069d2d
Download 3a8e4c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T10:11:57+01:00 Download 2a883ae
Download 2877c58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T09:42:49+01:00 Download 621ace0
Download b65e691 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T09:18:51+01:00 Download a077f32
Download 04f5c57 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T01:54 CET (sv-comp)
Download 48dbcb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:29 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1a7da26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 91 Sun Dec 3 02:05:04 2017
Download 473c211 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2017-12-02T00:58 CET (sv-comp)
Download 7ab3ce6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 17 2017-12-01T18:15:09.654459
Download 7250082 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 17 2017-12-01T13:35:15.676423
Download 0d180d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 43 2017-12-01T18:53 CET (sv-comp)
Download 2e56658 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 42 2017-12-01T03:51 CET (sv-comp)
Download 7698a60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 129 2017-11-30T15:39:55+01:00
Download 57ae264 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 78 2017-12-02T01:47:29+01:00
Download eb6b6af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 95 2017-11-30T12:44 CET (sv-comp)
Download 15e4bb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 78 2017-11-30T14:47 CET (sv-comp)
Download 4056bf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:46:13.257143
Download 2835b69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:53:00.355883
Download 33c951f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 166 2017-12-01T17:51 CET (sv-comp)
Download f22e811 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 64 2017-12-01T17:13 CET (sv-comp)

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

Trying to find witnesses for program (d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.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.1.ufo.BOUNDED-6.pals_true-termination.c, d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d15e6bc394d1dc7cd2d5b1ba5c602e7f8e6f406784c2b91595ac18d43b906fba.json

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