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 (5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6416647 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 126 2019-12-04T01:06 CET (comp)
Download a89f1e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-11T21:57:58+01:00 Download 2b727d6
Download 1f86782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 192 2019-12-11T20:44:48+01:00 Download 0835108
Download 0017b50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 190 2019-12-03T08:06:24+01:00 Download d479008
Download d479008 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 193 2019-11-30T05:16:15+01:00
Download 2b727d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 191 2019-12-01T00:43:30+01:00
Download 065edec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-11T21:09:10+01:00 Download 4365ea4
Download 46ce561 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-11T20:54:23+01:00 Download 8090464
Download e4d9c59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 35 2019-12-08T01:52:10+01:00 Download f6c7762
Download 27e9222 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-05T20:20:48+01:00 Download d754cc2
Download 8cde6c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-05T19:34:03+01:00 Download 20ef100
Download efb1920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 36 2019-12-04T02:58:24+01:00 Download 6416647
Download 9fb426d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 07:55:08

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

Trying to find witnesses for program (5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 65982e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T09:51 CET (sv-comp)
Download ed96983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 50 2018-12-08T03:58:39
Download 24c56a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 192 2018-12-07T10:23:44+01:00
Download cc3cf3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-08T23:44:34+01:00 Download 65982e7
Download 6267c55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-08T08:42:37+01:00 Download 24c56a8
Download fe2ffa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 190 2018-12-06T09:47:58+01:00 Download 1ba9bf6
Download 1ba9bf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 193 2018-12-05T15:40:49+01:00
Download 0aac318 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 35 2018-12-10T20:36:04+01:00 Download 609811f
Download f9ab775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 35 2018-12-09T18:22:53+01:00 Download 1e7a1e6
Download 80be670 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-08T22:08:39+01:00 Download ed96983
Download 52b2914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 35 2018-12-08T05:02:22+01:00 Download 274c39f
Download b3dd183 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-08T04:30:30+01:00 Download be38bd5
Download 758913e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 35 2018-12-06T10:20:12+01:00 Download 1325041
Download 2cc0389 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T09:40:44+01:00 Download ffa0945
Download bdb66a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T09:20:04+01:00 Download 5e64978

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

Trying to find witnesses for program (5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 9 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b4fb9cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 128 Sat Dec 2 20:50:22 2017
Download 10ea9a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2017-12-02T15:43 CET (sv-comp)
Download f2dc545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 24 2017-12-01T16:22:08.585694
Download fb5e07a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 24 2017-12-01T20:52:51.494792
Download f74242b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 61 2017-11-30T22:50 CET (sv-comp)
Download 8b115a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 189 2017-11-30T11:29:04+01:00
Download 1bfe02c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 112 2017-12-01T21:03:46+01:00
Download 3d3ca3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 134 2017-12-01T01:27 CET (sv-comp)
Download 86fc47b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 111 2017-11-30T12:50 CET (sv-comp)

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

Trying to find witnesses for program (5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

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

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