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 (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.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 (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.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 (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.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 (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.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 (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cddf2a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 5 2019-12-01 22:34:44
Download cdf83ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 102 2019-12-03T23:47 CET (comp)
Download d6d066d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 132 2019-12-11T21:43:56+01:00 Download bd67d3b
Download 227c4c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 138 2019-12-11T20:44:29+01:00 Download 33f2711
Download d80582d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 138 2019-12-08T01:51:27+01:00 Download f1d999a
Download 8efa6e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 134 2019-12-08T00:26:04+01:00 Download eda12cb
Download 2947ac6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 135 2019-12-07T21:18:14+01:00 Download 553b627
Download 82c6d59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 134 2019-12-03T08:08:25+01:00 Download 725326e
Download 725326e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 141 2019-11-30T00:08:13+01:00
Download f1d999a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 105 2019-12-07T13:41:53+01:00
Download bd67d3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 132 2019-12-01T16:02:25+01:00
Download a4d8b2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-11T21:09:09+01:00 Download cddf2a0
Download 770bcb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-11T20:54:20+01:00 Download a56b2d0
Download 3934167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-05T20:21:43+01:00 Download 0b09ac9
Download e35b27b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-05T19:34:22+01:00 Download df04f59
Download b2f6531 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-04T02:58:25+01:00 Download cdf83ce

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

Trying to find witnesses for program (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cb20e48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T11:29 CET (sv-comp)
Download b9418ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 42 2018-12-08T12:08:07
Download c996784 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 133 2018-12-06T13:15:04+01:00
Download a115952 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 133 2018-12-09T18:21:14+01:00 Download 20cf91f
Download 1cb1238 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 133 2018-12-08T23:44:46+01:00 Download cb20e48
Download 4a2f542 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 132 2018-12-08T08:39:27+01:00 Download c996784
Download 620c923 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 134 2018-12-06T09:49:02+01:00 Download cf10674
Download cf10674 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 141 2018-12-05T15:47:46+01:00
Download a690c93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-10T20:37:38+01:00 Download 9315b06
Download c64bab6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-09T20:53:24+01:00 Download dd9e588
Download dc8fa55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-09T20:40:07+01:00 Download 3f4a00c
Download 944388b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-08T22:07:54+01:00 Download b9418ec
Download 74b2eeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-08T05:02:32+01:00 Download 0aa2ed1
Download 958026d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-06T10:14:42+01:00 Download 9f9c3af
Download b9ab2ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-06T09:42:49+01:00 Download d0da5b0
Download 7b373f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-06T09:19:41+01:00 Download 0421841

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

Trying to find witnesses for program (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d8f2b18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 476 Sat Dec 2 21:15:42 2017
Download 300f7ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 181 2017-12-03T02:43Z
Download 19a247e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 6 2017-12-01T23:23 CET (sv-comp)
Download a191d56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 18 2017-12-01T15:49:21.829040
Download 65f9e40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 22 2017-12-01T15:33:46.830786
Download 0306ee7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 62 2017-11-30T22:43 CET (sv-comp)
Download 6f1d1da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 137 2017-12-01T03:49:29+01:00
Download e26b230 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 211 2017-11-30T13:13:27+01:00
Download d2aeba3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 66 2017-11-30T13:06:26+01:00
Download 356963d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 69 2017-12-02T13:25:06+01:00
Download 92a2b2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 108 2017-11-30T17:52 CET (sv-comp)
Download ea629c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 181 2017-12-02T18:34Z
Download 1a3492d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 105 2017-11-30T19:06 CET (sv-comp)

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

Trying to find witnesses for program (bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c, bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bfce00877f7b08447968e90718cded1fd740987807657cb10d131406d7c4c1df.json

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