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_inb_true-unreach-call_false-valid-memtrack.i |
programSHA | 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916 |
witnessName | results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | 380d76ffc940ef7bd20e1e0b491fe10b89de9ef9f5bc6a63d0b6e03b5500d391 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T14:54:22.478021 |
producer | ESBMC 4.6.0 kind |
program-sha256 | 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916 |
programfile | ../../sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i |
programhash | c169d08bbf77eaada0e2d433ba89b540e8f1bee9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/380d76ffc940ef7bd20e1e0b491fe10b89de9ef9f5bc6a63d0b6e03b5500d391.graphml |
witness-sha256 | 380d76ffc940ef7bd20e1e0b491fe10b89de9ef9f5bc6a63d0b6e03b5500d391 |
witness-size | 3422 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.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_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.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_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.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_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.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_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.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_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.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_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6c0f2eb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:09 CET (sv-comp) | ||
3ea3a44 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 6 | 2017-12-01T21:56 CET (sv-comp) | ||
9081f5f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:41 CET (sv-comp) | ||
a9607c7 | 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 | 43 | 2017-12-01T08:20 CET (sv-comp) | ||
7c8b61a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 39 | 2017-12-01T08:34:00+01:00 | ||
232698a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:19 CET (sv-comp) | ||
bb40dc6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 221 | 2017-12-03T03:00Z | ||
a048397 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T18:31 CET (sv-comp) | ||
64d79ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 213 | 2017-12-02T19:41Z | ||
380d76f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T14:54:22.478021 | ||
e0bd321 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 144 | 2017-12-02T19:57:57+01:00 | ||
7dd2ddd | 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 | 629b2a1 | |
187db93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-03T04:29:14+01:00 | c40ab1b | |
ff99433 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-03T02:40:10+01:00 | b639159 | |
c30b189 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-03T01:23:29+01:00 | c01d3cb | |
a67d028 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-02T20:06:47+01:00 | f553701 | |
2f1e9d5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-02T15:19:30+01:00 | ac0a86f | |
90f414d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-02T08:12:41+01:00 | 14e7d80 | |
43ad389 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-02T00:08:50+01:00 | 4c1a095 | |
5162bad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-01T07:12:43+01:00 | 7ffd5af | |
89a582f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-01T05:05:29+01:00 | 436d255 | |
69d6516 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-12-01T04:48:51+01:00 | ec752d2 | |
cd8db6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 125 | 2017-11-30T12:36:44+01:00 | ||
bd0553c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 5 | 2017-11-30T13:39:36+01:00 | ||
41fc7f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 144 | 2017-11-30T19:10:54+01:00 | ||
a182b38 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 4 | 2017-12-01T19:55:35+01:00 | ||
89419a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 221 | 2017-12-02T14:26Z |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i, 04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/04b079423f936f0e789f6990ed6fc202122e4738c952c42bae3ebe1f13add916.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |