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/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i
programSHA 9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd
witnessName results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.memleaks_test22_2_false-valid-memtrack_true-termination.i.files/witness.graphml
witnessSHA 29a3affc0ac42d4c4b55cad407051860117b0053d851bb9a6a47374d0d638b18

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/29a3affc0ac42d4c4b55cad407051860117b0053d851bb9a6a47374d0d638b18.json

Key Value
architecture 32bit
creationtime 2017-12-01T09:13 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd
programfile /tmp/vcloud-vcloud-master/worker/working_dir_5feb3402-9ca6-49c8-b1b4-aa06f424d352/sv-benchmarks/c/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i
programhash 20fbdf1deafb883d59b25bfdcd58a0b89c69ce87
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/29a3affc0ac42d4c4b55cad407051860117b0053d851bb9a6a47374d0d638b18.graphml
witness-sha256 29a3affc0ac42d4c4b55cad407051860117b0053d851bb9a6a47374d0d638b18
witness-size 8320
witness-type violation_witness

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

Trying to find witnesses for program (9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd, sv-benchmarks/c/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i).

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

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

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

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

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

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i, 9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3af0eb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T05:42 CET (sv-comp)
Download f379fb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T22:08:15+01:00 Download 831ac6d
Download ed944d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T09:01:28+01:00 Download f1226f6
Download 783c46e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T01:02:04+01:00
Download a964178 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T10:19:03+01:00 Download 58af43b
Download 7c44307 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:20:22+01:00 Download 88c90ef
Download f1226f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 10 2018-12-07T10:13:47+01:00
Download 26ec898 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T09:28:16+01:00 Download 5c18cd6
Download 831ac6d 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:21:00
Download f1794ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T23:43:43+01:00 Download 3af0eb8
Download 8f05162 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-07T01:19:07+01:00 Download 70ab72c
Download c24e877 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:49:15+01:00 Download 783c46e
Download ba33dcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T05:04:34+01:00 Download 3b3b0d8
Download b74a310 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-07T21:54 CET (sv-comp)

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

Trying to find witnesses for program (9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd, sv-benchmarks/c/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i).

Found 12 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i, 9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7f78b00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:38 CET (sv-comp)
Download 5c18cd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 5 2017-12-01T22:19 CET (sv-comp)
Download a8a02a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 2 2017-12-01T23:35 CET (sv-comp)
Download b93dde0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T08:24:24+01:00
Download 1fd1da6 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:30:43.184390
Download e56f4a6 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:19:34.334781
Download 29a3aff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 8 2017-12-01T09:13 CET (sv-comp)
Download 0ce0e5b 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 13 2017-12-01T08:30 CET (sv-comp)
Download 424a5c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:28:34.081519
Download 1462513 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:15:40.853769
Download de67af4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T20:15 CET (sv-comp)
Download b5cb227 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 10 2017-12-01T13:42 CET (sv-comp)

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

Trying to find witnesses for program (9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd, sv-benchmarks/c/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i, 9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9bf1d1079e470afbfe65468e50021c57d92563a9cefe1307f4af4ea8d720c1cd.json

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