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_product22_true-unreach-call_true-termination.cil.c |
programSHA | 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16 |
witnessName | results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.elevator_spec3_product22_true-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 63150247e5797af51281fb84317d6b084a6faadc778b80778783a921e6312c77 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T19:21 CET (sv-comp) |
producer | CBMC |
program-sha256 | 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16 |
programfile | ../../sv-benchmarks/c/product-lines/elevator_spec3_product22_true-unreach-call_true-termination.cil.c |
programhash | e4806982251c495754bfeb93d5bbb934373aeed4 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/63150247e5797af51281fb84317d6b084a6faadc778b80778783a921e6312c77.graphml |
witness-sha256 | 63150247e5797af51281fb84317d6b084a6faadc778b80778783a921e6312c77 |
witness-size | 583228 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.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_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.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_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.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_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.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_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.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_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 20 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e6c184f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T09:14 CET (sv-comp) | ||
b150232 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:52:02.159801 | ||
9f9f231 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T13:21:33.739130 | ||
9dafb61 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T16:56:24.822716 | ||
bb0413f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T20:40:01.108113 | ||
929d46f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 2051 | 2017-12-01T20:38 CET (sv-comp) | ||
e11c06c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 314 | 2017-12-02T20:31:42+01:00 | ||
0043c6f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T02:11:59+01:00 | ||
3ee8e63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 314 | 2017-12-03T04:08:13+01:00 | bad9c92 | |
d4e31b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 314 | 2017-12-02T20:51:13+01:00 | 40f89fc | |
76b83d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 314 | 2017-12-02T07:06:01+01:00 | 1d810fe | |
e1d06f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 314 | 2017-12-01T22:21:16+01:00 | d29737e | |
508ce9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 314 | 2017-12-01T08:14:10+01:00 | 975cdc4 | |
0d38228 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 314 | 2017-12-01T06:12:03+01:00 | d609f02 | |
4f1618f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 314 | 2017-12-01T05:04:09+01:00 | b1adee0 | |
b937cba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 315 | 2017-12-01T00:49:14+01:00 | ||
6315024 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 583 | 2017-11-30T19:21 CET (sv-comp) | ||
dd9223f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 28175 | 2017-11-30T19:24 CET (sv-comp) | ||
9a1fa4b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 583 | 2017-12-01T18:46 CET (sv-comp) | ||
316557f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 28179 | 2017-12-01T12:36 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product22_true-unreach-call_true-termination.cil.c, 7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7c5635c8b4d4b0e627b74a831fdd5057e8ff7e66f696047acbea544cecfdec16.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |