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/loops/while_infinite_loop_2_true-unreach-call_false-termination.i |
programSHA | 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2 |
witnessName | results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.while_infinite_loop_2_true-unreach-call_false-termination.i.files/witness.graphml |
witnessSHA | c5b08f9cc2ca4a5143354adef4c4a555824b8ce67c99ed06b36b55d1c6570c72 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T18:46:17.690061 |
producer | ESBMC 4.6.0 kind |
program-sha256 | 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2 |
programfile | ../../sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i |
programhash | 38eaba8d64f477684f2f9d73b6277bf5294da706 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/c5b08f9cc2ca4a5143354adef4c4a555824b8ce67c99ed06b36b55d1c6570c72.graphml |
witness-sha256 | c5b08f9cc2ca4a5143354adef4c4a555824b8ce67c99ed06b36b55d1c6570c72 |
witness-size | 3419 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3e24bf6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T13:10:11 | ||
07ef2fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 5 | 2018-12-07T09:02:30+01:00 | ||
c896d98 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T19:57:54+01:00 | 389a269 | |
7b57df2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T10:30:39+01:00 | 99d288d | |
8be39b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:19:55+01:00 | dde4441 | |
e63d0c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:08:37+01:00 | 19d4667 | |
18023ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T19:58:50+01:00 | 60faf12 | |
91a64b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T21:37:53+01:00 | 3e24bf6 | |
63d6c74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T07:13:54+01:00 | 07ef2fa | |
7969da4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T04:17:34+01:00 | 40d5a50 | |
b58d6b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T02:07:50+01:00 | 99d288d | |
2d8f38f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T17:44:44+01:00 | 85b2953 | |
7482516 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:28:21+01:00 | ff8292e | |
0ef3af7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:14:53+01:00 | cd8405c | |
b8b40a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T08:00:24+01:00 | e9cae65 | |
cd8405c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-05T13:46:08+01:00 | ||
281a4a0 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-07T20:42:18+01:00 | ||
32763df | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-05T21:23:54+01:00 |
Found 23 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
85b2953 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:16 CET (sv-comp) | ||
c917ae5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 5 | 2017-12-02T21:14Z | ||
81943aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 5 | 2017-12-02T10:55Z | ||
c5b08f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T18:46:17.690061 | ||
bb84d08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T16:39 CET (sv-comp) | ||
764c3ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 5 | 2017-12-02T19:32:30+01:00 | ||
73b9baa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T03:58:42+01:00 | ||
53287bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T01:37:41+01:00 | 0ae96d2 | |
0d6e0f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T14:38:39+01:00 | 2ee846c | |
979c6a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T07:53:43+01:00 | d850489 | |
464c77f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T00:15:14+01:00 | 7d83451 | |
02fd390 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T08:13:56+01:00 | 978185e | |
0303778 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T07:04:41+01:00 | 7b6cff4 | |
f616cea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:11:03+01:00 | d84d67e | |
aec66da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T03:54:14+01:00 | ||
8f0b822 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 6 | 2017-11-30T12:22:30+01:00 | ||
e99aad1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T23:42:26+01:00 | ||
a93b209 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 5 | 2017-12-01T19:20:53+01:00 | ||
9fa018c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 5 | 2017-12-02T18:43Z | ||
d3aa5dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 8 | 2017-12-01T03:10 CET (sv-comp) | ||
7b2d11e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T15:59:41+01:00 | ||
48ef298 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 5 | 2017-12-03T11:13Z | ||
e3435d2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 5 | 2017-12-01T15:16 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |