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.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c |
programSHA | 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8 |
witnessName | results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c.files/witness.graphml |
witnessSHA | a5cd26ff974c14870bb56b2b26bd9cb4bc2f5426839ba059a4fe9c4f0af9dac0 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T02:21 CET (sv-comp) |
memoryModel | precise |
producer | ESBMC 3.1 |
program-sha256 | 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_aa0b9b9d-5c7b-402d-b86b-3a0aed89d0b1/sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c |
programhash | 5ece07e091f918f26c76e2a65f38501df262220c |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/a5cd26ff974c14870bb56b2b26bd9cb4bc2f5426839ba059a4fe9c4f0af9dac0.graphml |
witness-sha256 | a5cd26ff974c14870bb56b2b26bd9cb4bc2f5426839ba059a4fe9c4f0af9dac0 |
witness-size | 61356 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.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.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.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.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.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.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
72a8fcc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 5 | 2019-12-02 05:11:51 | ||
8d8da22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 126 | 2019-12-04T00:53 CET (comp) | ||
215c0c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 186 | 2019-12-11T21:56:18+01:00 | 9e062e6 | |
0e6e0c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 181 | 2019-12-11T21:09:29+01:00 | 72a8fcc | |
c289c9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 181 | 2019-12-11T20:44:56+01:00 | 8902f79 | |
a5113c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 186 | 2019-12-03T08:10:34+01:00 | 01c2cd9 | |
01c2cd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 190 | 2019-11-29T22:14:15+01:00 | ||
9e062e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 187 | 2019-12-01T08:22:03+01:00 | ||
cc3ee5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-11T20:54:26+01:00 | 7a26f44 | |
2de1c12 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-08T01:51:19+01:00 | 231e1db | |
f66918f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-05T20:21:41+01:00 | 57fee6e | |
a0b8e2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-05T19:34:08+01:00 | b89e3e7 | |
cb58337 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-04T02:58:05+01:00 | 8d8da22 | |
0057b2c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 5 | 2019-12-02 05:21:08 | ||
6ffaa2a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T23:57 CET (comp) |
Found 17 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0f28455 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 10 | 2018-12-08T09:36 CET (sv-comp) | ||
63a3326 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 48 | 2018-12-08T10:27:57 | ||
4124732 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 189 | 2018-12-08T01:04:06+01:00 | ||
9d5b033 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 183 | 2018-12-09T20:34:58+01:00 | aa71dcc | |
8f4d9b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 181 | 2018-12-09T17:48:02+01:00 | 732446d | |
e2c62cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 181 | 2018-12-08T23:44:09+01:00 | 0f28455 | |
48585f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 187 | 2018-12-08T08:25:17+01:00 | 4124732 | |
e8bba72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 187 | 2018-12-06T09:49:01+01:00 | f166e39 | |
f166e39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 190 | 2018-12-06T02:10:53+01:00 | ||
0851b72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-10T20:37:47+01:00 | e4592d2 | |
38917ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-08T22:07:26+01:00 | 63a3326 | |
6035505 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-08T05:00:16+01:00 | 5fc4927 | |
69bdd3a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-06T10:19:17+01:00 | d0c2854 | |
8f59fb2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-06T09:42:23+01:00 | 4a6d422 | |
ca373b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-06T09:14:23+01:00 | d01e7ff | |
aa5c688 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:16 CET (sv-comp) | ||
0a41ed0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:16 CET (sv-comp) |
Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
080b840 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 132 | Sat Dec 2 20:59:31 2017 | ||
2d61f2f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 10 | 2017-12-02T01:02 CET (sv-comp) | ||
fc617f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 22 | 2017-12-01T18:46:11.400554 | ||
2f0dc0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 22 | 2017-12-01T10:45:12.677704 | ||
4feb82c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 62 | 2017-12-01T18:21 CET (sv-comp) | ||
a5cd26f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 61 | 2017-12-01T02:21 CET (sv-comp) | ||
fb06405 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 185 | 2017-12-01T02:45:08+01:00 | ||
38f5e69 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 106 | 2017-12-01T22:20:57+01:00 | ||
7090e5e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 142 | 2017-11-30T16:43 CET (sv-comp) | ||
c0e2e95 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 123 | 2017-12-01T01:47 CET (sv-comp) | ||
db6a94d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:25:43.303505 | ||
a0b1f01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:27:19.346064 | ||
206b923 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 267 | 2017-12-01T15:20 CET (sv-comp) | ||
edaba53 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 78 | 2017-12-01T13:30 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, 69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/69a55fb46997489dea6e84f3042fc69fe0e998e894e3262edf73125ffe94eaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |