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_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c |
programSHA | 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-cbmc.2018-12-06_0859.logfiles/sv-comp19_prop-reachsafety.pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA | d83e0a0749b28c95ac280ac274c9f34c366970e1e1ac4a410238f90c4b0b3fd8 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T09:14:53+01:00 |
inputwitnesshash | 3ca64dd5107aecbda912b2cf108242370b81179098513037c49b8b8e51be27d5 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464 |
programfile | ../../sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c |
programhash | 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d83e0a0749b28c95ac280ac274c9f34c366970e1e1ac4a410238f90c4b0b3fd8.graphml |
witness-sha256 | d83e0a0749b28c95ac280ac274c9f34c366970e1e1ac4a410238f90c4b0b3fd8 |
witness-size | 73326 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.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_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.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_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.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_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
484e994 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 451 | 2019-12-11T22:00:30+01:00 | 67a9c41 | |
1226ef4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 259 | 2019-12-11T20:44:57+01:00 | 74a19f9 | |
dccc2dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 210 | 2019-12-08T01:51:38+01:00 | b18a455 | |
fe95024 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 208 | 2019-12-03T08:10:27+01:00 | 39b68e5 | |
39b68e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 217 | 2019-11-30T03:37:23+01:00 | ||
b18a455 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 193 | 2019-12-07T15:55:07+01:00 | ||
67a9c41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 452 | 2019-12-01T08:41:58+01:00 | ||
1359633 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 73 | 2019-12-11T21:09:30+01:00 | 95bd17d | |
bfae424 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 73 | 2019-12-11T20:54:52+01:00 | 615c0fe | |
c5365d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 73 | 2019-12-07T21:12:38+01:00 | 6f654f9 | |
03a8346 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 73 | 2019-12-05T20:21:54+01:00 | a484bda | |
dd4ddc9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 73 | 2019-12-05T19:34:14+01:00 | 85ffe16 | |
0fabe75 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 5 | 2019-12-01 11:04:35 |
Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4432034 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 9 | 2018-12-08T14:27 CET (sv-comp) | ||
9ef5f9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 33 | 2018-12-08T14:30:35 | ||
f7fd60d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 460 | 2018-12-08T04:05:37+01:00 | ||
6d7eb23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 209 | 2018-12-09T18:20:20+01:00 | 30c53cb | |
3c7443c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 209 | 2018-12-08T23:42:05+01:00 | 4432034 | |
0753814 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 451 | 2018-12-08T08:36:01+01:00 | f7fd60d | |
96d321f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 208 | 2018-12-06T09:48:19+01:00 | c002623 | |
c002623 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 217 | 2018-12-05T11:17:04+01:00 | ||
1778f7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 73 | 2018-12-10T20:38:23+01:00 | 3364d19 | |
0ee5e7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-09T20:37:49+01:00 | 017ed8a | |
3f64190 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 73 | 2018-12-08T22:10:28+01:00 | 9ef5f9c | |
f818dc5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 73 | 2018-12-08T05:02:24+01:00 | 904dcee | |
772502b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 73 | 2018-12-06T10:18:58+01:00 | 298f33c | |
2e67089 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 73 | 2018-12-06T09:42:15+01:00 | 0d6698d | |
d83e0a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 73 | 2018-12-06T09:14:53+01:00 | 3ca64dd |
Found 10 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
83afcf6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 177 | Sat Dec 2 21:57:43 2017 | ||
4d89e4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 3 | 2017-12-02T01:00 CET (sv-comp) | ||
39a1752 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 26 | 2017-12-02T05:17:58.082558 | ||
53866b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 18 | 2017-12-01T08:25:53.964759 | ||
592fdfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 69 | 2017-12-01T07:11 CET (sv-comp) | ||
739a81e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 209 | 2017-11-30T22:30:02+01:00 | ||
e8407fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 291 | 2017-12-01T00:34:25+01:00 | ||
fda71e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 261 | 2017-11-30T12:58 CET (sv-comp) | ||
65853a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 243 | 2017-12-02T11:50Z | ||
08c3e0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 91 | 2017-12-01T02:33 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/20f78f287fc66a356f10d5e41093b5871648750c677d2d9a838a993421614464.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |