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/mix031_power.opt_false-unreach-call.i |
programSHA | 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb |
witnessName | results-verified/uautomizer.2018-12-08_0742.logfiles/sv-comp19_prop-reachsafety.mix031_power.opt_false-unreach-call.i.files/witness.graphml |
witnessSHA | 2d994597026e1ca83d6dd206313a5a756dcae5b9ed8c144fa6977613113abe65 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T07:23Z |
producer | Automizer |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_14cb6ad0-fe55-477b-a652-3ebf1f6a8234/sv-benchmarks/c/pthread-wmm/mix031_power.opt_false-unreach-call.i |
programhash | a86cc350d743297ef1f0c4e735f7c78846f139ec |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/2d994597026e1ca83d6dd206313a5a756dcae5b9ed8c144fa6977613113abe65.graphml |
witness-sha256 | 2d994597026e1ca83d6dd206313a5a756dcae5b9ed8c144fa6977613113abe65 |
witness-size | 56777 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.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/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.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/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.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/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.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/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/pthread-wmm/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c0a3676 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-07T23:31:45 | ||
a16e9af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 20 | 2018-12-08T03:30:12+01:00 | ||
cb6a657 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-09T21:47:53+01:00 | 3661fe1 | |
073d8a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-09T21:38:31+01:00 | 49c0505 | |
3949e52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-08T08:04:14+01:00 | a16e9af | |
ae5014b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 77 | 2018-12-08T04:58:13+01:00 | 9b56c62 | |
76cbbd8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 108 | 2018-12-08T03:34:21+01:00 | 4c0d230 | |
be130d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T19:52:48+01:00 | 17539d0 | |
35e3868 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 77 | 2018-12-06T10:18:12+01:00 | 2ec7c46 | |
18d94db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-06T09:48:38+01:00 | ac650c5 | |
ea5def8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 108 | 2018-12-06T09:17:06+01:00 | 03f713c | |
6e430b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 108 | 2018-12-06T09:00:24+01:00 | 03f713c | |
ac650c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T05:52:00+01:00 | ||
2ebc16e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-09T20:53:25+01:00 | ffd7391 | |
703c9a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-09T20:38:56+01:00 | 2d99459 | |
6bd6583 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-08T22:08:47+01:00 | c0a3676 |
Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
abec40e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Yogar-CBMC 1.0 | 14 | 2017-12-03T05:35 CET (sv-comp) | ||
43dec55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T14:48:39.147342 | ||
313a6d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-02T01:20:09.178206 | ||
f40b761 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 21 | 2017-12-01T12:34 CET (sv-comp) | ||
ebe3d89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-01T10:09:41+01:00 | ||
03f713c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 3 | 2017-12-01T09:58 CET (sv-comp) | ||
cbeabf2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 17 | 2017-12-01T08:48:24+01:00 | aa19c6e | |
527961b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 14 | 2017-12-01T08:46:35+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix031_power.opt_false-unreach-call.i, 7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7d806b570a0f7a9c07088b5489e6cfe860241747ab26a1cfdc66e45e100fb9fb.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |