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/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c |
programSHA | f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d |
witnessName | results-verified/divine-smt.2018-12-06_1106.logfiles/sv-comp19_prop-reachsafety.elevator_spec3_product31_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 4049604289fbc07865c474e775e492abf85a99c5f2563dbf77245b86a5c998b6 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T13:36 CET (sv-comp) |
memorymodel | precise |
producer | DIVINE 4 |
programfile | ../../sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c |
programhash | e4c8b021dd10e17f75bc3f05209475156561c2f7 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/4049604289fbc07865c474e775e492abf85a99c5f2563dbf77245b86a5c998b6.graphml |
witness-sha256 | 4049604289fbc07865c474e775e492abf85a99c5f2563dbf77245b86a5c998b6 |
witness-size | 4355 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1bf690c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 14:42:48 | ||
adea8cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 195 | 2019-12-03T23:18 CET (comp) | ||
94df3e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 335 | 2019-12-11T21:42:21+01:00 | 8a33388 | |
f39c63e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 336 | 2019-12-11T21:09:44+01:00 | 1bf690c | |
0dea506 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 335 | 2019-12-11T20:54:30+01:00 | 2a7e2cc | |
a93fc20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 336 | 2019-12-11T20:44:29+01:00 | 90b4048 | |
79e2a0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 335 | 2019-12-08T01:51:53+01:00 | df35be0 | |
05dc9b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 335 | 2019-12-04T02:58:31+01:00 | adea8cb | |
db76555 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 335 | 2019-12-03T08:56:52+01:00 | 6662bbe | |
db20774 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 335 | 2019-12-03T08:09:37+01:00 | bbc3227 | |
bbc3227 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 296 | 2019-11-29T14:20:14+01:00 | ||
df35be0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 338 | 2019-12-07T22:22:43+01:00 | ||
8a33388 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 296 | 2019-11-30T20:59:04+01:00 | ||
bdf6329 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 323 | 2019-12-05T20:20:26+01:00 | 362ad7d | |
7e5c96a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 323 | 2019-12-05T19:34:28+01:00 | 8ce369d | |
3ed7c56 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:10 CET (comp) |
Found 22 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e032b49 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T00:40 CET (sv-comp) | ||
f1fec21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 59 | 2018-12-08T01:44:39 | ||
3403896 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 220 | 2018-12-06T22:13 CET (sv-comp) | ||
9366ba9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 308 | 2018-12-10T17:41:00+01:00 | ||
ca778ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 337 | 2018-12-07T11:02:35+01:00 | ||
70cb97d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-10T20:38:28+01:00 | 9366ba9 | |
5be9cd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-10T10:48:45+01:00 | 4049604 | |
ea2e3b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-09T17:52:00+01:00 | d03a393 | |
202df5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-08T23:42:12+01:00 | e032b49 | |
73aaad1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 208 | 2018-12-08T22:10:28+01:00 | f1fec21 | |
bf3978f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-08T07:58:50+01:00 | ca778ba | |
e7c103e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-08T04:54:41+01:00 | 45efcab | |
0f363b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-08T04:29:32+01:00 | 4049604 | |
1713f8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-07T17:45:15+01:00 | 3403896 | |
60d4960 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-06T10:17:26+01:00 | df4e282 | |
4b009a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 335 | 2018-12-06T09:48:40+01:00 | 7c0eeb3 | |
7c0eeb3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 296 | 2018-12-05T21:01:48+01:00 | ||
6d90b7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 323 | 2018-12-06T09:42:45+01:00 | 16f44da | |
3eb771d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 323 | 2018-12-06T09:19:55+01:00 | ec928e2 | |
4a59c7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 323 | 2018-12-06T09:07:06+01:00 | cf4518f | |
ac20211 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:11 CET (sv-comp) | ||
9534f87 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T05:37 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c, f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f9f71569320291c5b9e096c9a7ea529da8e092d90e6f9396e800e27d7eb2659d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |