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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 08480c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 420 2019-12-11T21:42:57+01:00 Download b32650a
Download 690ce9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 399 2019-12-11T20:44:35+01:00 Download 73151ad
Download 68fa8e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 420 2019-12-03T08:09:06+01:00 Download 5362350
Download 5362350 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 429 2019-11-30T11:06:02+01:00
Download b32650a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 421 2019-12-01T18:14:45+01:00
Download 5d23593 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 62 2019-12-11T20:54:51+01:00 Download ecbd6c9
Download c6f4b28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 64 2019-12-08T01:51:19+01:00 Download ee2ca06
Download 1107fd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 62 2019-12-05T20:21:19+01:00 Download 7e03d82
Download 6be564d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 64 2019-12-05T19:34:26+01:00 Download 372e9d0

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f9b0fbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 14 2018-12-08T07:40 CET (sv-comp)
Download 908bf52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 99 2018-12-08T05:04:27
Download 5ed189f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 425 2018-12-07T21:54:18+01:00
Download 0c9f340 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 399 2018-12-09T18:12:37+01:00 Download 64e54ff
Download 0e62010 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 405 2018-12-08T23:43:59+01:00 Download f9b0fbe
Download 4c0c447 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 420 2018-12-08T07:59:53+01:00 Download 5ed189f
Download c59d410 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 420 2018-12-06T09:48:05+01:00 Download 9086aa9
Download 9086aa9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 429 2018-12-05T17:49:14+01:00
Download 2b68bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 64 2018-12-10T20:35:52+01:00 Download 890a3e2
Download f2a269c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 62 2018-12-08T22:10:28+01:00 Download 908bf52
Download cd0004d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 64 2018-12-08T05:06:13+01:00 Download 46b8497
Download 2be60b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 64 2018-12-06T10:19:50+01:00 Download 9e96914
Download 57e4ac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 64 2018-12-06T09:42:15+01:00 Download 0eb1795
Download 0bda738 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 62 2018-12-06T09:18:59+01:00 Download 2f7f964

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e10085f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 283 Sun Dec 3 00:20:11 2017
Download abcf14e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 14 2017-12-02T07:44 CET (sv-comp)
Download eb3bfd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 46 2017-12-01T20:13:04.529346
Download 0d7d665 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 47 2017-12-01T16:37:04.692275
Download bacf6dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 120 2017-12-01T02:55 CET (sv-comp)
Download 75abe8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 411 2017-11-30T17:58:59+01:00
Download cc6351e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 296 2017-11-30T11:39 CET (sv-comp)
Download a57d5e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 240 2017-11-30T15:44 CET (sv-comp)

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

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

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

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