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/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c |
programSHA | 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9 |
witnessName | results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c.files/witness.graphml |
witnessSHA | bedf00c9ed6f61bfc56663e9d4ff07db7a73bf2df95822de404a93ce7338dcb4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T00:09:37+01:00 |
producer | CPAchecker 1.7-svn b8d6131600+ |
program-sha256 | 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9 |
programfile | ../../sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c |
programhash | 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/bedf00c9ed6f61bfc56663e9d4ff07db7a73bf2df95822de404a93ce7338dcb4.graphml |
witness-sha256 | bedf00c9ed6f61bfc56663e9d4ff07db7a73bf2df95822de404a93ce7338dcb4 |
witness-size | 118634 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b7bc4a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 4 | 2019-12-01 08:27:28 | ||
355e194 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 81 | 2019-12-04T00:59 CET (comp) | ||
a9bb10d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 122 | 2019-12-11T21:57:15+01:00 | f8230d6 | |
06596d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T21:40:27+01:00 | 6fdca59 | |
fc76d8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 114 | 2019-12-11T21:09:06+01:00 | b7bc4a1 | |
91dc839 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 114 | 2019-12-11T20:44:32+01:00 | 15c9990 | |
26abaf4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 115 | 2019-12-07T21:18:39+01:00 | e8f08fd | |
579a2c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 121 | 2019-12-03T08:57:12+01:00 | 3243c28 | |
88551e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-03T08:10:29+01:00 | 2153264 | |
2153264 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 120 | 2019-11-30T07:28:25+01:00 | ||
6fdca59 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 118 | 2019-12-01T08:08:47+01:00 | ||
9788e90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 32 | 2019-12-11T20:54:53+01:00 | 62afab7 | |
e0b987e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 33 | 2019-12-08T01:51:19+01:00 | 7975215 | |
5c18289 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 32 | 2019-12-05T20:20:49+01:00 | 01d71c3 | |
0282fc0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 33 | 2019-12-05T19:34:13+01:00 | 6e5bf78 | |
6dd92bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 32 | 2019-12-04T02:58:25+01:00 | 355e194 | |
2fb07ce | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 4 | 2019-12-01 14:20:38 | ||
80341d2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:39 CET (comp) |
Found 18 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d34bd99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2018-12-08T16:05 CET (sv-comp) | ||
9821c6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 30 | 2018-12-08T12:02:48 | ||
bedf00c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 119 | 2018-12-07T00:09:37+01:00 | ||
3e61050 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 115 | 2018-12-09T20:19:21+01:00 | 6a1adbc | |
ef83785 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 114 | 2018-12-09T18:00:23+01:00 | 5a42474 | |
01ad731 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 114 | 2018-12-08T23:43:46+01:00 | d34bd99 | |
2b70de3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T08:03:21+01:00 | bedf00c | |
f00d153 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 121 | 2018-12-08T04:26:56+01:00 | 0235b3b | |
c3b3b67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-06T09:48:26+01:00 | 51c553c | |
51c553c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 120 | 2018-12-06T05:28:32+01:00 | ||
0d265d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-10T20:38:13+01:00 | 8d4e4cb | |
be5de8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 32 | 2018-12-08T22:09:14+01:00 | 9821c6e | |
a81cf71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-08T05:01:27+01:00 | 6f6d641 | |
7589da9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-06T10:18:18+01:00 | 7e3df7e | |
eb4baf6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-06T09:42:42+01:00 | 373a649 | |
f392e38 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 32 | 2018-12-06T09:12:26+01:00 | c6320ab | |
f31252a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:51 CET (sv-comp) | ||
358fb46 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T08:42 CET (sv-comp) |
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7d42091 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 87 | Sat Dec 2 20:56:04 2017 | ||
f663f64 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2017-12-02T18:53 CET (sv-comp) | ||
457d6bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 16 | 2017-12-01T17:49:18.688877 | ||
e3c2d57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 16 | 2017-12-01T16:18:38.142043 | ||
957e2ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 41 | 2017-12-01T16:35 CET (sv-comp) | ||
c45f4be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 39 | 2017-12-01T02:03 CET (sv-comp) | ||
006094e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 117 | 2017-11-30T19:18:38+01:00 | ||
206de52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 75 | 2017-12-02T03:30:57+01:00 | ||
5f87235 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 76 | 2017-11-30T16:22 CET (sv-comp) | ||
e51abfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:10:39.309795 | ||
835af46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:24:02.640796 | ||
290a892 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 160 | 2017-12-01T17:53 CET (sv-comp) | ||
38783ca | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 62 | 2017-12-01T13:34 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c, 71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/71694ae9a454cae533ffd828882dcff283006b532fd076a89e3d0680ca3747c9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |