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_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c |
programSHA | b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23 |
witnessName | results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c.files/witness.graphml |
witnessSHA | b1b67df11747d26dc47159f5db4d5480e565d6dcb17c2aa8b0836eddf094bb1c |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T18:19 CET (sv-comp) |
memoryModel | precise |
producer | ESBMC 3.1 |
program-sha256 | b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_f5532814-d33b-4d6d-a003-48d4973078ac/sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c |
programhash | b3b24d22acbd30abb2bd6c739c1741063240b31f |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/b1b67df11747d26dc47159f5db4d5480e565d6dcb17c2aa8b0836eddf094bb1c.graphml |
witness-sha256 | b1b67df11747d26dc47159f5db4d5480e565d6dcb17c2aa8b0836eddf094bb1c |
witness-size | 40568 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.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_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.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_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.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_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d63bf3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 5 | 2019-12-01 16:21:48 | ||
6fed6e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 61 | 2019-12-03T23:25 CET (comp) | ||
a4db661 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 76 | 2019-12-11T21:39:43+01:00 | 2b41fe0 | |
4c733c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 76 | 2019-12-11T20:55:21+01:00 | dec8861 | |
52a6e94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 76 | 2019-12-11T20:44:39+01:00 | 5cd3266 | |
554d202 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 76 | 2019-12-08T01:52:11+01:00 | 8115bb4 | |
3e3cbc2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 79 | 2019-12-08T00:26:03+01:00 | 0ac8f70 | |
a3f8ea2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 79 | 2019-12-07T21:13:16+01:00 | b946a94 | |
3c4bb89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 76 | 2019-12-03T08:10:18+01:00 | 8ebf756 | |
8ebf756 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 70 | 2019-11-30T01:24:26+01:00 | ||
8115bb4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 57 | 2019-12-07T15:20:43+01:00 | ||
2b41fe0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 75 | 2019-11-30T21:17:41+01:00 | ||
0e3ad4a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 83 | 2019-12-11T21:09:40+01:00 | d63bf3f | |
bf4f90f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 83 | 2019-12-05T20:20:51+01:00 | 3d04c17 | |
76f5783 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 83 | 2019-12-05T19:34:01+01:00 | a162201 | |
e320aa4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 83 | 2019-12-04T02:58:21+01:00 | 6fed6e0 |
Found 17 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bb42810 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2018-12-08T13:20 CET (sv-comp) | ||
46c88ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 28 | 2018-12-08T04:07:51 | ||
51579e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 76 | 2018-12-07T01:16:46+01:00 | ||
31e73bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 79 | 2018-12-09T20:53:08+01:00 | d42c03e | |
65ba964 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 79 | 2018-12-09T20:37:38+01:00 | 1378633 | |
b2c4227 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 76 | 2018-12-09T18:21:07+01:00 | b0d05c0 | |
a7ec9d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 76 | 2018-12-08T23:42:21+01:00 | bb42810 | |
9270877 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 76 | 2018-12-08T08:56:24+01:00 | 51579e1 | |
1aa6e52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 76 | 2018-12-08T05:02:11+01:00 | 00cc729 | |
02f405e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 76 | 2018-12-08T04:19:06+01:00 | 3621a75 | |
8b52ff5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 76 | 2018-12-06T10:18:36+01:00 | 06db584 | |
28dce4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 76 | 2018-12-06T09:48:12+01:00 | cad9534 | |
cad9534 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 70 | 2018-12-06T06:57:37+01:00 | ||
f020c1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 83 | 2018-12-10T20:36:20+01:00 | e529e1f | |
f2b9940 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 83 | 2018-12-08T22:09:42+01:00 | 46c88ff | |
43c64b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 83 | 2018-12-06T09:40:39+01:00 | 33ecbff | |
e909e83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 83 | 2018-12-06T09:09:34+01:00 | 98e50bb |
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4424167 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 59 | Sun Dec 3 01:36:34 2017 | ||
e9c6207 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 112 | 2017-12-03T02:39Z | ||
1c24e15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 6 | 2017-12-02T07:56 CET (sv-comp) | ||
b5e6f63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 13 | 2017-12-02T04:51:27.746645 | ||
7756865 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 10 | 2017-12-01T18:27:44.786508 | ||
b1b67df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 41 | 2017-11-30T18:19 CET (sv-comp) | ||
3adb778 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 70 | 2017-11-30T15:32:10+01:00 | ||
ee956a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 130 | 2017-11-30T23:37:22+01:00 | ||
d02c3b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 39 | 2017-11-30T17:48:32+01:00 | ||
30f9506 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 41 | 2017-12-02T13:43:56+01:00 | ||
472fbf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 63 | 2017-11-30T23:48 CET (sv-comp) | ||
156a75e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 112 | 2017-12-02T07:24Z | ||
cfddd32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 64 | 2017-12-01T01:46 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c, b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b8ad7169559aa9b47f2ec0042781c45c12256c55ff8d7665e40c13bc192ddd23.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |