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 (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.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 (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.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 (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.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 (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.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 (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.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 '19

Trying to find witnesses for program (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.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 '18

Trying to find witnesses for program (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 13 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e3c6392 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 15 2017-12-02T00:23:18+01:00
Download bc6ff56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 1210 2017-12-02T23:53Z
Download 6ffe7d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:03:38.761929
Download 10c90ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 461 2017-12-03T07:04:34+01:00 6084ac4
Download d5d4338 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 461 2017-12-03T01:54:44+01:00 0f1fdc3
Download 042f324 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 461 2017-12-02T08:06:08+01:00 1c8c7aa
Download e0375e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 461 2017-12-01T07:01:39+01:00 e3d0fe2
Download a7ce483 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 461 2017-12-01T06:48:23+01:00 00ffc93
Download 84ce28b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 461 2017-12-01T05:00:21+01:00 3280dc0
Download 6e0f167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 461 2017-11-30T21:28:13+01:00
Download 763ecbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 283 2017-12-01T03:08:34+01:00
Download 77f9cb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 461 2017-12-01T02:28:33+01:00
Download 897c11e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 1304 2017-12-02T18:22Z

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

Trying to find witnesses for program (d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d52335ec835e154f1e94e6ffdb122c7b3d03babfc2aeb47ea7b8c45956c1ef1d.json

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