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/array-memsafety/cstrcat_unsafe_false-valid-deref.i
programSHA 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
witnessName results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.cstrcat_unsafe_false-valid-deref.i.files/witness.graphml
witnessSHA ffbab33f15a94a6a0f860f5620b40d417a09fcc838d416365aae3f8e4b8f6761

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-03T06:53Z
error-specification-length Key 'specification' longer than 100 characters.
producer Taipan
program-sha256 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
programfile /tmp/vcloud-vcloud-master/worker/working_dir_40c3c708-74da-41e6-91bc-38f19520e0f5/sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i
programhash 8bca29efe4e2caa04afbd06c4ca0de4d513af778
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/ffbab33f15a94a6a0f860f5620b40d417a09fcc838d416365aae3f8e4b8f6761.graphml
witness-sha256 ffbab33f15a94a6a0f860f5620b40d417a09fcc838d416365aae3f8e4b8f6761
witness-size 4513
witness-type violation_witness

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

Trying to find witnesses for program (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.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 (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.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 (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.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 (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.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 (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.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 (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 17 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7783c34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:48:43+01:00 Download 7f5a606
Download 033692b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:19:11+01:00 Download 34bfb11
Download 6533f01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T08:15:46+01:00 Download adfa781
Download 130af87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:02:58+01:00 Download 7f5a606
Download dcddd0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T10:18:46+01:00 Download 1a020b2
Download 9ac6c5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:19:51+01:00 Download 5890f7d
Download 2af8c19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-05T19:35:28+01:00
Download adfa781 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T12:48:20+01:00
Download a0d67e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:38:06+01:00 Download cf83007
Download 66e922c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T22:10:44+01:00 Download eb3a208
Download 3b481c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-07T09:21:31+01:00 Download 4955938
Download 151c2ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:48:38+01:00 Download 2af8c19
Download eb3a208 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-08T20:11:15
Download 33f5d5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:53:12+01:00 Download f5ce8dd
Download 8a6b6c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:04:44+01:00 Download 659e7a8
Download 4632d71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-07T01:07:54+01:00 Download 7f2fdc0
Download 7ee21d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:00:24+01:00 Download 1667187

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

Trying to find witnesses for program (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 11 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fc65739 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:32 CET (sv-comp)
Download b85c8a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:30:30+01:00
Download c991b0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T12:04:00.749570
Download c829027 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:46:57.945087
Download 921a77a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:15 CET (sv-comp)
Download ffbab33 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 Taipan 5 2017-12-03T06:53Z
Download ebe66b2 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 Kojak 5 2017-12-03T03:54Z
Download 3217723 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 4 2017-12-01T08:30 CET (sv-comp)
Download 25eae97 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 Automizer 4 2017-12-03T04:09Z
Download 4955938 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T22:17 CET (sv-comp)
Download ce632d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 3 2017-12-01T23:35 CET (sv-comp)

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

Trying to find witnesses for program (60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb, sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrcat_unsafe_false-valid-deref.i, 60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/60ca96450c1631277820b9dc4201dd261068695b6812eda48f4262e0b3e294bb.json

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