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 (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.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 (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.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 (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.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 (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.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 (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.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 (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 7 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e6ab2a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T02:57 CET (sv-comp)
Download 9cb0f9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 84 2018-12-08T04:00:21+01:00
Download 68946e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T02:16 CET (sv-comp)
Download dd490dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T19:00:46
Download 0b0d761 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 84 2018-12-07T13:14:27+01:00
Download 5f0d4c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 84 2018-12-05T21:39:51+01:00
Download fc0844f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:48 CET (sv-comp)

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

Trying to find witnesses for program (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 18 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ff58b0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-02T23:48 CET (sv-comp)
Download 90ef9d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T10:40:11.933361
Download c010472 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 3.1 307 2017-12-01T09:55 CET (sv-comp)
Download 3aaccd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 207 2017-12-03T06:54Z
Download 0ce1622 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 514 2017-12-03T04:14Z
Download 3aaec27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 207 2017-12-03T03:55Z
Download b038649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 1058 2017-12-01T08:21 CET (sv-comp)
Download fcf54ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 13 2017-12-02T07:03:58+01:00
Download bd17319 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 209 2017-12-03T03:34Z
Download 5e360e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T00:13 CET (sv-comp)
Download 60d58d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T02:13:16.691678
Download 82baddd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 307 2017-12-01T19:48 CET (sv-comp)
Download a599602 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 84 2017-11-30T12:44:52+01:00
Download bea338b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 196 2017-12-01T02:14:23+01:00
Download 7d20aac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 84 2017-12-01T00:24:55+01:00
Download da3a500 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 208 2017-12-02T19:14Z
Download 5125d00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 1045 2017-11-30T20:15 CET (sv-comp)
Download 6d49b0c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 1045 2017-12-01T16:09 CET (sv-comp)

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

Trying to find witnesses for program (b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8, sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c, b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b2bfb71b67fe1a4c4497e15116605552238b599065f23efa9e28da9868e9b8e8.json

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