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/triangular_false-unreach-call.i |
programSHA | 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-uautomizer.2018-12-09_2030.logfiles/sv-comp19_prop-reachsafety.triangular_false-unreach-call.i.files/witness.graphml |
witnessSHA | d444160dc5965625c05c5de3e9417c568e65b58983fab24202e4a4da227e6cb1 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T20:41:30+01:00 |
inputwitnesshash | e36ff1d1920c5b567dc245a29f17607906cbabb6867cb9d05f9cec0fff5396f1 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46 |
programfile | ../../sv-benchmarks/c/pthread/triangular_false-unreach-call.i |
programhash | 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d444160dc5965625c05c5de3e9417c568e65b58983fab24202e4a4da227e6cb1.graphml |
witness-sha256 | d444160dc5965625c05c5de3e9417c568e65b58983fab24202e4a4da227e6cb1 |
witness-size | 3701 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46).
Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3dc1653 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 16 | 2018-12-07T10:52:13+01:00 | ||
385d0a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-10T10:48:48+01:00 | ab7a466 | |
098adaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T21:49:40+01:00 | 6a8f184 | |
916c907 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T21:38:33+01:00 | 56f1471 | |
0eb42d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T08:27:15+01:00 | 3dc1653 | |
068a40f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T04:35:39+01:00 | ab7a466 | |
9c01cf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T19:53:38+01:00 | 5fcf854 | |
46e95d5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:47:55+01:00 | 575170b | |
99143eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:18:40+01:00 | 9b6dd55 | |
bcee55f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:00:05+01:00 | 9b6dd55 | |
575170b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T00:29:42+01:00 | ||
ae2104c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:54:17+01:00 | 314d0a4 | |
d444160 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:41:30+01:00 | e36ff1d |
Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |