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/memsafety/test-0158_false-valid-memtrack_true-termination.i
programSHA 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
witnessName results-verified/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.test-0158_false-valid-memtrack_true-termination.i.files/witness.graphml
witnessSHA 98913d6782195a960d7b51da111e2942967b62c492b2de2ef345279572839970

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/98913d6782195a960d7b51da111e2942967b62c492b2de2ef345279572839970.json

Key Value
architecture 32bit
creationtime 2017-12-02T11:42:07.308906
producer ESBMC 4.6.0 kind
program-sha256 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
programfile ../../sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i
programhash 9b3e50b8f852fe8799cb6ad900b216b16bf216ae
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/98913d6782195a960d7b51da111e2942967b62c492b2de2ef345279572839970.graphml
witness-sha256 98913d6782195a960d7b51da111e2942967b62c492b2de2ef345279572839970
witness-size 3623
witness-type violation_witness

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

Trying to find witnesses for program (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.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 (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.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 (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.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 (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.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 (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.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 (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 19 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download afb24d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T12:24 CET (sv-comp)
Download c45c447 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T01:02:22+01:00
Download ab2d614 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T22:07:31+01:00 Download f21727d
Download 1daf9af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:49:04+01:00 Download 258637e
Download 5e15ac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:19:39+01:00 Download bb08600
Download bcd8675 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:14:43+01:00 Download b7411cd
Download 258637e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T05:36:26+01:00
Download 83f528e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T05:02:55+01:00 Download fe8ae67
Download 84888f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T10:16:19+01:00 Download 75f4821
Download 7dc48cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:42:28+01:00 Download c5b6d54
Download a9b8d8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:44:50+01:00 Download afb24d2
Download aa96bd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T07:48:24+01:00 Download c45c447
Download d109ef4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-07T09:17:38+01:00 Download 4a72b92
Download f21727d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness SMACK 1.9.3 3 2018-12-08T06:02:31
Download 4bafbea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:48:51+01:00 Download 3626fe3
Download 85f7e98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:13:08+01:00 Download 3626fe3
Download 2b6e415 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-07T01:12:25+01:00 Download c0fe3bb
Download e970c44 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T17:46 CET (sv-comp)
Download 813c320 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:59 CET (sv-comp)

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

Trying to find witnesses for program (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 14 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 88cd8f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:01 CET (sv-comp)
Download 4a72b92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 4 2017-12-01T22:17 CET (sv-comp)
Download 732eb72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 2 2017-12-01T23:45 CET (sv-comp)
Download 28f3137 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:29:58+01:00
Download 98913d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T11:42:07.308906
Download 05d31e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T23:43:53.373335
Download a21880c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:21 CET (sv-comp)
Download f2f71e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 5 2017-12-01T08:24 CET (sv-comp)
Download c1cd5f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness 2LS 3 2017-12-01T08:25 CET (sv-comp)
Download 71f707e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:20:47.665854
Download 0db1c5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:21:02.099597
Download ee7a969 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T20:40 CET (sv-comp)
Download 3cec7f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T16:16 CET (sv-comp)
Download 10e182e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 10 2017-12-01T12:27 CET (sv-comp)

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

Trying to find witnesses for program (2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d, sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0158_false-valid-memtrack_true-termination.i, 2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2538245f4923b6f7047a3f57da6c55ee0b2b22e5262acc5b3477a8536505591d.json

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