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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i
programSHA 92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7
witnessName results-verified/forester.2017-12-01_1912.logfiles/sv-comp18.sll-circular_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA 8a162e2df0c1549c6bcfba5b63d0dc91d30ee7e093e132a246e6d071e5c07645

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8a162e2df0c1549c6bcfba5b63d0dc91d30ee7e093e132a246e6d071e5c07645.json

Key Value
architecture 32bit
creationtime 2017-12-01T19:23 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
memorymodel precise
producer Forester
program-sha256 92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7
programfile ../../sv-benchmarks/c/forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i
programhash 811c06b4616c360d68e825b8fa9e0b4596e5faf8
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/8a162e2df0c1549c6bcfba5b63d0dc91d30ee7e093e132a246e6d071e5c07645.graphml
witness-sha256 8a162e2df0c1549c6bcfba5b63d0dc91d30ee7e093e132a246e6d071e5c07645
witness-size 34733
witness-type correctness_witness

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

Trying to find witnesses for program (92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7, sv-benchmarks/c/forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ebf170b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 10 2019-12-01T13:29:53+01:00
Download 5d4150c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 10 2019-11-30T14:06:19+01:00
Download 9e88a18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-07T23:46:21+01:00 Download 27ff72e
Download 5fe27b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-11-30T17:07:51+01:00 Download 2155387
Download 2155387 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 12 2019-11-30T10:05:41+01:00

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

Trying to find witnesses for program (92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7, sv-benchmarks/c/forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i).

Found 9 witnesses for program sv-benchmarks/c/forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i, 92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae78103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 10 2018-12-07T07:53:34+01:00
Download 8fc5d15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T07:40:32+01:00
Download acf8cfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T10:49:32
Download 70cb3a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 11 2018-12-07T08:18:16+01:00
Download a9fca0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T21:53:29+01:00 Download acf8cfa
Download e70ebf2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T07:04:07+01:00 Download 70cb3a7
Download a331680 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-07T09:07:12+01:00 Download 9db720f
Download 64be98e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:29:55+01:00 Download a404e11
Download a404e11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T07:22:12+01:00

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

Trying to find witnesses for program (92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7, sv-benchmarks/c/forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8a162e2 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 35 2017-12-01T19:23 CET (sv-comp)
Download c347706 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T20:37:20+01:00
Download 9db720f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:31 CET (sv-comp)
Download bbbb8c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Forester 35 2017-12-01T18:07 CET (sv-comp)
Download f3bade1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T21:19:39+01:00 559a811
Download aedee50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T18:47:20+01:00 e10ab1f
Download 9db9679 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T07:29:00+01:00 b622b3e
Download 773ad6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 12 2017-12-01T00:52:00+01:00

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

Trying to find witnesses for program (92b15ee82015dc1847fe1f058c54921fcfd0400d80614f8b06ce74475e1327e7, sv-benchmarks/c/forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i).

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

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