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).
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.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/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.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/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.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/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.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/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 12 witnesses for program sv-benchmarks/c/pthread-wmm/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1a7df09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T15:52:11 | ||
19aa5f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 26 | 2018-12-07T09:04:22+01:00 | ||
96db745 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T21:48:12+01:00 | 837cea4 | |
7136426 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T21:38:37+01:00 | 7d4ca44 | |
e1c5d2a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-08T08:18:17+01:00 | 19aa5f4 | |
ae0afbf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-08T05:01:40+01:00 | 89b2dd9 | |
0ada401 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T19:53:56+01:00 | a7cb465 | |
6fd36ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-06T10:18:17+01:00 | 798911d | |
3748818 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-06T09:49:15+01:00 | 1d1da47 | |
1d1da47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-05T20:28:03+01:00 | ||
870d222 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-06T09:11:55+01:00 | 468c23b | |
18694c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-06T09:11:16+01:00 | 468c23b |
Found 6 witnesses for program sv-benchmarks/c/pthread-wmm/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4238f8d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 17 | 2017-12-03T05:42 CET (sv-comp) | ||
1137c22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 27 | 2017-12-01T11:20 CET (sv-comp) | ||
d6ab5d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 24 | 2017-12-01T10:07:49+01:00 | ||
468c23b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 4 | 2017-12-01T10:11 CET (sv-comp) | ||
0ad916d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 35 | 2017-12-01T08:48:24+01:00 | c78efb6 | |
acec338 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 17 | 2017-12-01T08:46:24+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix001_rmo.opt_false-unreach-call.i, c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c0cb96850fc665a5ef4b61d58d9eec21bdac1261016e742b39b52ae0d56af0e3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |