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.UNBOUNDED.pals.c |
programSHA | a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56 |
witnessName | results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA | 29e5b1453ae5962334ec5aa83fffd3891f71120d0cd4ac2d9bce73afa5c7f2a9 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T12:56 CET (sv-comp) |
producer | CBMC |
program-sha256 | a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56 |
programfile | ../../sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c |
programhash | d52e74df0654e1f032e9591db582096a56c19f5c |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/29e5b1453ae5962334ec5aa83fffd3891f71120d0cd4ac2d9bce73afa5c7f2a9.graphml |
witness-sha256 | 29e5b1453ae5962334ec5aa83fffd3891f71120d0cd4ac2d9bce73afa5c7f2a9 |
witness-size | 86004 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.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.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.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.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.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.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 17 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
41f972a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 80 | 2019-12-04T00:40 CET (comp) | ||
c205d01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 112 | 2019-12-11T21:58:06+01:00 | 0f81d30 | |
bc71232 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 114 | 2019-12-11T21:44:20+01:00 | ea9e391 | |
02525d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 114 | 2019-12-11T20:44:50+01:00 | 2380c50 | |
a4722a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 117 | 2019-12-08T01:51:57+01:00 | 20cb2c8 | |
4a98298 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 112 | 2019-12-07T21:14:50+01:00 | 409e7fb | |
e9b3651 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-03T08:57:33+01:00 | 984d46f | |
172d0a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 117 | 2019-12-03T08:07:32+01:00 | 7d8dd46 | |
7d8dd46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 120 | 2019-11-30T02:27:57+01:00 | ||
20cb2c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 93 | 2019-12-07T14:10:31+01:00 | ||
ea9e391 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 115 | 2019-12-01T00:55:30+01:00 | ||
ff8e805 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 32 | 2019-12-11T21:09:33+01:00 | 0ec7326 | |
77bf1e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 32 | 2019-12-11T20:55:21+01:00 | 020304c | |
48b6303 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 32 | 2019-12-05T20:20:26+01:00 | 00c1335 | |
9ffe352 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 33 | 2019-12-05T19:34:25+01:00 | 161eca6 | |
f741ee5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 33 | 2019-12-04T02:58:15+01:00 | 41f972a | |
206a876 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 4 | 2019-12-01 10:38:30 |
Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5bb2fd7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2018-12-08T03:23 CET (sv-comp) | ||
98c552f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 29 | 2018-12-08T00:40:58 | ||
193c3b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 115 | 2018-12-08T02:31:35+01:00 | ||
7d5b127 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 112 | 2018-12-09T20:27:45+01:00 | 55e0fc3 | |
edb40f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 114 | 2018-12-09T18:21:04+01:00 | 0f94912 | |
8d66bee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 111 | 2018-12-08T23:43:08+01:00 | 5bb2fd7 | |
5fbbc38 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 114 | 2018-12-08T08:55:29+01:00 | 193c3b6 | |
9862df8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T03:48:39+01:00 | ed4b2a9 | |
ba866bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 117 | 2018-12-06T09:49:19+01:00 | 7a03601 | |
7a03601 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 120 | 2018-12-05T10:54:05+01:00 | ||
2744fd6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-10T20:37:43+01:00 | ff1d21b | |
2d3479c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 32 | 2018-12-08T22:10:45+01:00 | 98c552f | |
c811a62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-08T04:59:07+01:00 | 67e71d4 | |
d5cc022 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-06T10:18:08+01:00 | 6a185eb | |
01b2f8f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-06T09:41:48+01:00 | 180f32a | |
d19786a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 32 | 2018-12-06T09:16:36+01:00 | 3b74133 |
Found 10 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
368fe88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 82 | Sun Dec 3 00:35:53 2017 | ||
938c1d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2017-12-02T05:07 CET (sv-comp) | ||
1a6a1dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 141 | 2017-12-02T16:45Z | ||
fd79170 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 15 | 2017-12-02T01:10:57.166562 | ||
4274a5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 16 | 2017-12-01T20:32:53.944414 | ||
fcc4731 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 39 | 2017-11-30T16:33 CET (sv-comp) | ||
d18f413 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-11-30T14:58:05+01:00 | ||
3c48fe9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 74 | 2017-12-01T22:45:01+01:00 | ||
29e5b14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 86 | 2017-11-30T12:56 CET (sv-comp) | ||
d32efcf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 72 | 2017-11-30T16:09 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |