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/pthread-wmm/mix041_rmo.opt_false-unreach-call.i |
programSHA | 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4 |
witnessName | results-verified/esbmc-kind.2017-12-02_1345.logfiles/sv-comp18.mix041_rmo.opt_false-unreach-call.i.files/witness.graphml |
witnessSHA | d6c951e1ad5c2c7a45f805e2d106792b21e24c1363ec33eeeb2c69a66a3253bf |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T16:38:41.911629 |
producer | ESBMC 4.6.0 kind |
program-sha256 | 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4 |
programfile | ../../sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i |
programhash | f7f00b8a2e26669f3416c65156e30bcc7eb97f9e |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d6c951e1ad5c2c7a45f805e2d106792b21e24c1363ec33eeeb2c69a66a3253bf.graphml |
witness-sha256 | d6c951e1ad5c2c7a45f805e2d106792b21e24c1363ec33eeeb2c69a66a3253bf |
witness-size | 3598 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 17 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cd4f198 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T05:29:22 | ||
f8b4547 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 23 | 2018-12-06T13:23:35+01:00 | ||
1e0dad9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 257 | 2018-12-10T10:49:05+01:00 | f2725ba | |
9977f8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-09T21:47:46+01:00 | 215f2d4 | |
6b704aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T21:38:25+01:00 | 36524b2 | |
a933154 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-08T08:26:31+01:00 | f8b4547 | |
0e1dd20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-08T05:06:07+01:00 | 27ffeed | |
65b11b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 257 | 2018-12-08T03:59:28+01:00 | f2725ba | |
1a93d97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T19:53:18+01:00 | 78eb649 | |
17deeba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 57 | 2018-12-06T10:19:06+01:00 | ee9068b | |
b447b74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-06T09:48:06+01:00 | 5a0a4ea | |
46398ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-06T09:13:25+01:00 | 698bdbb | |
362ff6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-06T09:00:48+01:00 | 698bdbb | |
5a0a4ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-05T23:32:53+01:00 | ||
d199dc7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-09T20:53:37+01:00 | 665d1a6 | |
f8baab4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-09T20:39:51+01:00 | d368ec3 | |
531ca39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-08T22:08:51+01:00 | cd4f198 |
Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ce5e104 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 14 | 2017-12-03T06:14 CET (sv-comp) | ||
d6c951e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T16:38:41.911629 | ||
6a7630b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-02T03:53:25.416787 | ||
e9df09a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 21 | 2017-12-01T10:46 CET (sv-comp) | ||
900e60a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T10:32:58+01:00 | ||
698bdbb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 3 | 2017-12-01T10:23 CET (sv-comp) | ||
b2e8f89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 34 | 2017-12-01T08:48:24+01:00 | df08879 | |
620f2ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 96 | 2017-12-01T08:46:37+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix041_rmo.opt_false-unreach-call.i, 9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9f13537b19a2ec2e8742f566cae2f12165e4d0b3de3812b06cc1db549c1de4b4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |