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/nec20_false-unreach-call_true-termination.i |
programSHA | 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120 |
witnessName | results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.nec20_false-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | 3303da38eed19a0deca0e503cd29498d9d82cb842b8b37c3026dfc41075e3b68 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T21:55 CET (sv-comp) |
memoryModel | precise |
producer | ESBMC 3.1 |
program-sha256 | 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_520297ce-711f-4af9-9c6f-b3bf4af711c3/sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i |
programhash | 8f5e55a4b7a22c3d7de3d0a49a2ff34f668b1e90 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/3303da38eed19a0deca0e503cd29498d9d82cb842b8b37c3026dfc41075e3b68.graphml |
witness-sha256 | 3303da38eed19a0deca0e503cd29498d9d82cb842b8b37c3026dfc41075e3b68 |
witness-size | 5016 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 24 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7c4d33b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2018-12-08T07:42 CET (sv-comp) | ||
47da1ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T04:55:04 | ||
85593a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 23 | 2018-12-07T01:58 CET (sv-comp) | ||
5d7a56c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 8 | 2018-12-10T18:09:33+01:00 | ||
a767de1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 9 | 2018-12-06T23:57:03+01:00 | ||
b4d94d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-10T20:35:49+01:00 | 5d7a56c | |
ac7af54 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T21:23:34+01:00 | c614509 | |
c469b4e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:53:05+01:00 | f2bd11d | |
4796f86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:39:11+01:00 | c78053c | |
02f4e8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:16:47+01:00 | c536499 | |
a9e7bcb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1274 | 2018-12-09T17:57:01+01:00 | 03ce82e | |
a4741d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1274 | 2018-12-08T23:44:56+01:00 | 7c4d33b | |
0f75b88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T22:11:09+01:00 | 47da1ff | |
79ec0e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T09:05:45+01:00 | a767de1 | |
5c0e3ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T05:02:25+01:00 | 948fd31 | |
b75f99e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T18:48:02+01:00 | 8a41009 | |
2278a3a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T17:44:37+01:00 | 85593a7 | |
e289085 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T10:12:17+01:00 | 899e8e3 | |
42ed053 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:48:56+01:00 | b9e80e9 | |
e1e0833 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:10:31+01:00 | ccb6cbd | |
b9e80e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T02:17:02+01:00 | ||
d0fc341 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:40:49+01:00 | 88870c9 | |
41b1dcb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:00:48+01:00 | 7896e6f | |
395447d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:33 CET (sv-comp) |
Found 20 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
84accc7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T23:27 CET (sv-comp) | ||
b18a7da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 9 | 2017-12-03T00:23Z | ||
5cf0008 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T14:32 CET (sv-comp) | ||
25794ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 9 | 2017-12-02T17:17Z | ||
8ac003d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T04:45:52.622923 | ||
196502b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T20:14:46.281240 | ||
ce8952c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T19:34 CET (sv-comp) | ||
3303da3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-11-30T21:55 CET (sv-comp) | ||
5168ded | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 9 | 2017-12-02T21:05:08+01:00 | ||
96621b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-11-30T19:26:01+01:00 | ||
b2ef604 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 11 | 2017-11-30T21:57:06+01:00 | ||
ffd8668 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 6 | 2017-11-30T20:03:22+01:00 | ||
7d1a59b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 7 | 2017-12-01T23:05:02+01:00 | ||
00d48a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 28 | 2017-11-30T17:56 CET (sv-comp) | ||
a4e6dd4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 9 | 2017-12-02T10:25Z | ||
1c7ccbe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 7 | 2017-11-30T22:47 CET (sv-comp) | ||
57a29dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:53:23.934407 | ||
5bb1655 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T13:06:53.221269 | ||
3a07626 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 938 | 2017-12-01T14:39 CET (sv-comp) | ||
51c5681 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 14 | 2017-12-01T15:48 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |