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-verified/lazycseq.2018-12-06_1210.logfiles/sv-comp19_prop-reachsafety.triangular_false-unreach-call.i.files/witness.graphml |
witnessSHA | 5fcf8543b691c70942b185d6b9900d8e48eaf876dd643199708f977bee0e5bfa |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T11:15:25 |
producer | CSeq |
programfile | ../../sv-benchmarks/c/pthread/triangular_false-unreach-call.c |
programhash | 726f30e3329fddbca1ef0820468f0134fa5bc7c4d17ef89739ac6e37dae4af19 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/5fcf8543b691c70942b185d6b9900d8e48eaf876dd643199708f977bee0e5bfa.graphml |
witness-sha256 | 5fcf8543b691c70942b185d6b9900d8e48eaf876dd643199708f977bee0e5bfa |
witness-size | 4250 |
witness-type | violation_witness |
This witness was created for a different program (cf. table above, 726f30e3329fddbca1ef0820468f0134fa5bc7c4d17ef89739ac6e37dae4af19).
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 |