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 (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.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 (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.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 (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.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 (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.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 (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 5 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8ca9d0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 17 2019-11-29T18:18:09+01:00
Download 220e391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 17 2019-12-01T09:31:33+01:00
Download c0409c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 17 2019-12-07T23:47:04+01:00 Download 88907db
Download 7fc6afd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 17 2019-11-30T17:28:58+01:00 Download 18b2bf4
Download 18b2bf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 18 2019-11-30T12:35:33+01:00

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

Trying to find witnesses for program (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 7 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b12763a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 17 2018-12-07T09:05:29+01:00
Download 6965182 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T10:51:16
Download ccd528a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 18 2018-12-07T14:52:10+01:00
Download 0c54397 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 18 2018-12-08T05:52:37+01:00 Download ccd528a
Download de5807d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-07T09:07:20+01:00 Download c2c160a
Download 24fcd87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 18 2018-12-06T08:59:57+01:00 Download b143594
Download b143594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 18 2018-12-05T20:50:31+01:00

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

Trying to find witnesses for program (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 8 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c8dc5c2 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 Forester 128 2017-12-01T19:48 CET (sv-comp)
Download e29869e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T13:15:15+01:00
Download c2c160a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:40 CET (sv-comp)
Download a7089e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Forester 128 2017-12-01T18:21 CET (sv-comp)
Download 6510d23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 17 2017-12-01T21:18:25+01:00 76c0ec4
Download fb36af3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 17 2017-12-01T18:48:34+01:00 43d5210
Download 24302d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 17 2017-12-01T06:25:52+01:00 9e31d06
Download 019b100 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 27 2017-11-30T11:53:03+01:00

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

Trying to find witnesses for program (5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b, sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i, 5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5a24471fc37a392b619db0796a8fd5d51a3491cce16a0c68a0ae7792d83bc17b.json

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