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/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i
programSHA 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
witnessName results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i.files/witness.graphml
witnessSHA 554c69bfa7d8baf897eacfd2c6a052df44dd7ffd7f06737f1957c95ff5eea177

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T08:23 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
producer CBMC
program-sha256 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
programfile ../../sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i
programhash b370e5a1203ca56910126e51b2fc199b0ec5c281
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/554c69bfa7d8baf897eacfd2c6a052df44dd7ffd7f06737f1957c95ff5eea177.graphml
witness-sha256 554c69bfa7d8baf897eacfd2c6a052df44dd7ffd7f06737f1957c95ff5eea177
witness-size 44248
witness-type violation_witness

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

Trying to find witnesses for program (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.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 (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.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 (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.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 (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.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 (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.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 (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.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 '18

Trying to find witnesses for program (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 27 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 374cd0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:17 CET (sv-comp)
Download d8230b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 6 2017-12-01T21:58 CET (sv-comp)
Download 8a1a48c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 3 2017-12-01T23:33 CET (sv-comp)
Download 8668214 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 39 2017-12-01T08:29:47+01:00
Download 554c69b 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 44 2017-12-01T08:23 CET (sv-comp)
Download 555cefe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:50 CET (sv-comp)
Download 917956f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 221 2017-12-03T03:20Z
Download 343a000 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T17:15 CET (sv-comp)
Download 15da41e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 213 2017-12-02T08:54Z
Download 2e3187a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T23:04:59.787836
Download f7c842b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 144 2017-12-03T03:00:14+01:00
Download 9dd1731 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-03T06:50:46+01:00 ccca4a6
Download f93b34f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-03T04:29:58+01:00 4964910
Download 5527e77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-03T01:02:40+01:00 ec7f1f2
Download dd095ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T23:34:19+01:00 04bb6d0
Download ca21fa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T19:59:17+01:00 0f495a9
Download 712011c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T15:20:00+01:00 e846839
Download 609603f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T08:55:21+01:00 6931354
Download a64a788 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T00:11:22+01:00 a9781da
Download a7b4b63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T07:00:39+01:00 b00ee17
Download a330843 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T06:10:39+01:00 aab7ad4
Download 96c9430 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T04:24:48+01:00 ca8ec43
Download 0563bc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T00:32:32+01:00
Download c894c52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 5 2017-11-30T23:15:01+01:00
Download 0175553 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 144 2017-11-30T18:19:19+01:00
Download 688414e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-02T02:38:43+01:00
Download 8139d06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 221 2017-12-02T18:11Z

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

Trying to find witnesses for program (0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i, 0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0b8ad55e03e32f066cc764be76f0546e7b0f98f9e3464249c6c09962370713c8.json

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