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 (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.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 (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.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 (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.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 (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.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 (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 4 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3400b01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 26 2019-11-29T18:28:06+01:00
Download b95a11e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 26 2019-11-30T21:25:39+01:00
Download b3a7857 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 31 2019-11-29T22:53:52+01:00
Download 66addea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 31 2019-12-01T07:08:49+01:00

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

Trying to find witnesses for program (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 11 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4a4f5ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:04:47
Download 25029aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 27 2018-12-07T02:02:54+01:00
Download d61ea82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-09T20:34:12+01:00 Download 896d4f9
Download d7b273d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-09T17:24:24+01:00 Download e16de96
Download 88d5206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-08T21:56:13+01:00 Download 4a4f5ed
Download ab7b60f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-08T05:48:45+01:00 Download 25029aa
Download 73d4a8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-06T09:39:15+01:00 Download ca8c9d2
Download a7e6703 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-06T09:18:12+01:00 Download 811e6b2
Download 811e6b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 26 2018-12-05T14:15:26+01:00
Download 9af6574 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 31 2018-12-07T12:14:29+01:00
Download c2f29d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 31 2018-12-05T10:42:26+01:00

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

Trying to find witnesses for program (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 10 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 63a1f82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 27 2017-12-03T02:24:40+01:00 62d94e5
Download 356fd76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 27 2017-12-02T15:05:57+01:00 cefdef4
Download c7a6d92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 27 2017-12-01T06:44:32+01:00 fa2df69
Download 256529b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 27 2017-12-01T06:07:11+01:00 88d096c
Download 8271f56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 26 2017-11-30T14:35:59+01:00
Download d06a8b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 61 2017-11-30T13:55:29+01:00
Download c187880 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 7 2017-12-02T01:48:23+01:00
Download 2374c7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 43 2017-12-02T17:13Z
Download bf6b3b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 31 2017-12-01T17:38:14+01:00
Download 5636f35 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 24 2017-12-03T11:12Z

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

Trying to find witnesses for program (fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3, sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c, fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/fbbe6e30f73d96e6f930a72bebf93230bb070f84f076b541a600dbc7f3160fb3.json

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