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_4_false-unreach-call_true-termination.i |
programSHA | 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b |
witnessName | results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.while_infinite_loop_4_false-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | 09ad22bdbb5639521643ee83bc1523e3a2ff70305eca3eb1762b48f86170150e |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T22:05 CET (sv-comp) |
memorymodel | simple |
producer | skink |
program-sha256 | 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b |
programfile | ../../sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i |
programhash | 66fc6b12b7cd24de7373fe06aeeb5aec1e7e0e8b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/09ad22bdbb5639521643ee83bc1523e3a2ff70305eca3eb1762b48f86170150e.graphml |
witness-sha256 | 09ad22bdbb5639521643ee83bc1523e3a2ff70305eca3eb1762b48f86170150e |
witness-size | 2562 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.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_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.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_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.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_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.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_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 27 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4ac0779 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T05:46 CET (sv-comp) | ||
9baa140 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T08:33:40 | ||
381d47b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 5 | 2018-12-07T01:04 CET (sv-comp) | ||
67dd730 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 5 | 2018-12-10T17:10:50+01:00 | ||
d278768 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 5 | 2018-12-07T19:06:58+01:00 | ||
3758082 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T20:34:56+01:00 | 67dd730 | |
28cdbb8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:58+01:00 | 56501c9 | |
70dc314 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:53:26+01:00 | 1e9b592 | |
a960ec1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:39:16+01:00 | 57583b8 | |
dcaeb16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:23:13+01:00 | 0b0f86c | |
fafb5ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T17:58:56+01:00 | 8b2e561 | |
126a92e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:42:12+01:00 | 4ac0779 | |
3a9ccb0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T22:09:00+01:00 | 9baa140 | |
d84a756 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T07:47:29+01:00 | d278768 | |
eb6f976 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T05:06:08+01:00 | d26102a | |
95e5081 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:37:04+01:00 | 56501c9 | |
82b3caf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T18:47:04+01:00 | b750eb7 | |
fb0c451 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T17:43:20+01:00 | 381d47b | |
42578af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T01:10:18+01:00 | da84b8b | |
85caea9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T10:13:38+01:00 | b4fae12 | |
bc49067 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:48:18+01:00 | c077626 | |
4da9b15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:06:06+01:00 | cd11533 | |
8f8417e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:00:15+01:00 | 4729a5c | |
c077626 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T07:10:22+01:00 | ||
0a3c977 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:40:46+01:00 | 2d427ee | |
89dfd15 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:47 CET (sv-comp) | ||
c2d61f7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:20 CET (sv-comp) |
Found 21 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
09ad22b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:05 CET (sv-comp) | ||
44746a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 6 | 2017-12-02T17:33Z | ||
259ee94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T17:46 CET (sv-comp) | ||
1e1f0f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T21:45 CET (sv-comp) | ||
356b8ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 6 | 2017-12-02T20:36Z | ||
1321aaf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T01:12:34.198404 | ||
3ff78e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T14:29:00.575158 | ||
26423e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T19:51 CET (sv-comp) | ||
4aaad7e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-11-30T21:14 CET (sv-comp) | ||
556071d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 6 | 2017-12-03T02:15:44+01:00 | ||
b160316 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-11-30T19:17:54+01:00 | ||
197561b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 7 | 2017-11-30T16:00:08+01:00 | ||
5ff78c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-11-30T20:41:17+01:00 | ||
cb3d7be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 6 | 2017-12-01T22:31:39+01:00 | ||
e44419c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 4 | 2017-12-01T01:46 CET (sv-comp) | ||
38cdf25 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 6 | 2017-12-02T08:23Z | ||
2d427ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 4 | 2017-11-30T13:52 CET (sv-comp) | ||
d7529da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T21:53:09.233452 | ||
a00217f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:56:09.158634 | ||
b8794d9 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 6 | 2017-12-01T11:53 CET (sv-comp) | ||
2f09956 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T13:46 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |