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_test18_3_false-valid-memtrack_true-termination.i
programSHA 5f7d22f7c8ba85b94fa067bb3c1f65fbe22b5573e48e345578dfe396c1065886
witnessName results-validated/cpa-seq-validate-violation-witnesses-symbiotic.2018-12-08_2340.logfiles/sv-comp19_prop-memsafety.memleaks_test18_3_false-valid-memtrack_true-termination.i.files/witness.graphml
witnessSHA baa4f7d9eb5c6974048c6a9de6c77b8aab7568ecd7b7fc3060287f2c51b24fb9

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/baa4f7d9eb5c6974048c6a9de6c77b8aab7568ecd7b7fc3060287f2c51b24fb9.json

Key Value
architecture 32bit
creationtime 2018-12-08T23:43:55+01:00
inputwitnesshash 9194d464782f6c08581d2b49039d845241c57d21204397c73bc543c72289a5f1
producer CPAchecker 1.7-svn 29852
program-sha256 5f7d22f7c8ba85b94fa067bb3c1f65fbe22b5573e48e345578dfe396c1065886
programfile ../../sv-benchmarks/c/ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i
programhash 5f7d22f7c8ba85b94fa067bb3c1f65fbe22b5573e48e345578dfe396c1065886
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-deref) )
witness-file witnessFileByHash/baa4f7d9eb5c6974048c6a9de6c77b8aab7568ecd7b7fc3060287f2c51b24fb9.graphml
witness-sha256 baa4f7d9eb5c6974048c6a9de6c77b8aab7568ecd7b7fc3060287f2c51b24fb9
witness-size 31461
witness-type violation_witness

This witness was created for this program (cf. table above, 5f7d22f7c8ba85b94fa067bb3c1f65fbe22b5573e48e345578dfe396c1065886).

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

Trying to find witnesses for program (5f7d22f7c8ba85b94fa067bb3c1f65fbe22b5573e48e345578dfe396c1065886, sv-benchmarks/c/ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i).

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9194d46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-07T21:43 CET (sv-comp)
Download aa20ecd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 31 2018-12-07T16:46:09+01:00
Download 65dc902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 31 2018-12-06T09:49:01+01:00 Download 6fcea99
Download 6fcea99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 31 2018-12-05T09:52:07+01:00
Download aac768b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T05:05:59+01:00 Download bd75112
Download c685467 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 31 2018-12-08T08:26:39+01:00 Download aa20ecd
Download 8611589 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 31 2018-12-07T09:13:32+01:00 Download 0824cda
Download 6cce2b0 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-08T07:55:36
Download baa4f7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 31 2018-12-08T23:43:55+01:00 Download 9194d46
Download dcdcb2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 31 2018-12-08T22:11:18+01:00 Download 6cce2b0
Download 6d37a86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-07T01:08:58+01:00 Download 03df5fb
Download c8512de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-06T10:21:08+01:00 Download 2dd1815
Download c540015 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:07 CET (sv-comp)
Download 7cf8250 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T23:55 CET (sv-comp)

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

Trying to find witnesses for program (5f7d22f7c8ba85b94fa067bb3c1f65fbe22b5573e48e345578dfe396c1065886, sv-benchmarks/c/ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 92d2e1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:41 CET (sv-comp)
Download 0824cda Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 7 2017-12-01T21:53 CET (sv-comp)
Download 23a2c30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 5 2017-12-01T23:20 CET (sv-comp)
Download 5f1681d 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:52:37.029948
Download 098b780 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:30:27.280272
Download cf2000b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 10 2017-12-01T09:32 CET (sv-comp)
Download 04e83ed 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 43 2017-12-01T08:28 CET (sv-comp)
Download 19e0a31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.6.1-svn 26773 30 2017-12-01T08:34:53+01:00
Download 54e00bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:14:53.950050
Download d8d3e0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:17:25.240818
Download 5d2fd3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T20:44 CET (sv-comp)
Download ca12899 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 29 2017-12-01T16:24 CET (sv-comp)

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

Trying to find witnesses for program (5f7d22f7c8ba85b94fa067bb3c1f65fbe22b5573e48e345578dfe396c1065886, sv-benchmarks/c/ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i).

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

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