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-atomic/read_write_lock_false-unreach-call.i |
programSHA | 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-yogar-cbmc.2018-12-09_2138.logfiles/sv-comp19_prop-reachsafety.read_write_lock_false-unreach-call.i.files/witness.graphml |
witnessSHA | b2c292090bb66df1c7f5862597981d4f8abff76e5146fa620ebdaac3760442c5 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T21:38:37+01:00 |
inputwitnesshash | 4fb9f9cc4c025d01878d21a1e8db8adf50360431670cf45cfdc2b5069690d8f9 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8 |
programfile | ../../sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i |
programhash | 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/b2c292090bb66df1c7f5862597981d4f8abff76e5146fa620ebdaac3760442c5.graphml |
witness-sha256 | b2c292090bb66df1c7f5862597981d4f8abff76e5146fa620ebdaac3760442c5 |
witness-size | 9507 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8).
Found 0 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 14 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a9018c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:12:48 | ||
df88aaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T09:47:54+01:00 | ||
8dcbf4f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T21:47:35+01:00 | 43903ff | |
b2c2920 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-09T21:38:37+01:00 | 4fb9f9c | |
f7c86c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T08:39:15+01:00 | df88aaa | |
2d478c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T19:53:15+01:00 | bedab4d | |
ddb06b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:47:56+01:00 | 54bb1d7 | |
2af7ea7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:17:37+01:00 | 423982a | |
54bb1d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-05T08:06:48+01:00 | ||
d24ac22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:49:18+01:00 | 0c3b29b | |
d3942fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:11:13+01:00 | a9018c2 | |
079b379 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T04:57:53+01:00 | 9cae7e2 | |
64e59af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T04:37:21+01:00 | 0c3b29b | |
be3f4be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T10:17:35+01:00 | 7dbc476 |
Found 0 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-atomic/read_write_lock_false-unreach-call.i, 3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3752a1e6ef58fb71d6a9db94c344e4c3447ecb0048ba36b85f6e6e0342a0bca8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |