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).
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/predatorhp.2017-12-01_2145.logfiles/sv-comp18.ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | d8230b63a1840457dfbddc67a9c30a3f0f38674d796d7cde6389b49bfc34bc94 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T21:58 CET (sv-comp) |
memorymodel | precise |
producer | PredatorHP |
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-memtrack) ) |
witness-file | witnessFileByHash/d8230b63a1840457dfbddc67a9c30a3f0f38674d796d7cde6389b49bfc34bc94.graphml |
witness-sha256 | d8230b63a1840457dfbddc67a9c30a3f0f38674d796d7cde6389b49bfc34bc94 |
witness-size | 6128 |
witness-type | violation_witness |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
374cd0f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:17 CET (sv-comp) | ||
d8230b6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 6 | 2017-12-01T21:58 CET (sv-comp) | ||
8a1a48c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:33 CET (sv-comp) | ||
8668214 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 39 | 2017-12-01T08:29:47+01:00 | ||
554c69b | Inspect | 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) | ||
555cefe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:50 CET (sv-comp) | ||
917956f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 221 | 2017-12-03T03:20Z | ||
343a000 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T17:15 CET (sv-comp) | ||
15da41e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 213 | 2017-12-02T08:54Z | ||
2e3187a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T23:04:59.787836 | ||
f7c842b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 144 | 2017-12-03T03:00:14+01:00 | ||
9dd1731 | Inspect | 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 | |
f93b34f | Inspect | 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 | |
5527e77 | Inspect | 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 | |
dd095ef | Inspect | 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 | |
ca21fa6 | Inspect | 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 | |
712011c | Inspect | 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 | |
609603f | Inspect | 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 | |
a64a788 | Inspect | 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 | |
a7b4b63 | Inspect | 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 | |
a330843 | Inspect | 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 | |
96c9430 | Inspect | 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 | |
0563bc6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-01T00:32:32+01:00 | ||
c894c52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 5 | 2017-11-30T23:15:01+01:00 | ||
0175553 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 144 | 2017-11-30T18:19:19+01:00 | ||
688414e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 4 | 2017-12-02T02:38:43+01:00 | ||
8139d06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 221 | 2017-12-02T18:11Z |
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 |