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/loop-acceleration/underapprox_false-unreach-call2_true-termination.i |
programSHA | 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466 |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-reachsafety.underapprox_false-unreach-call2_true-termination.i.files/witness.graphml |
witnessSHA | 31438eee2b726419e906f0b1b8cf46c6d314c943eeac9047f45947dae75545ec |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T13:20 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_cad6bfa4-36dd-4269-942a-5d5e0e9ff4ce/sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i |
programhash | 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/31438eee2b726419e906f0b1b8cf46c6d314c943eeac9047f45947dae75545ec.graphml |
witness-sha256 | 31438eee2b726419e906f0b1b8cf46c6d314c943eeac9047f45947dae75545ec |
witness-size | 830 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466).
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 28 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
31438ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T13:20 CET (sv-comp) | ||
b7df11e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T11:28:23 | ||
9cfebcd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 10 | 2018-12-07T11:02 CET (sv-comp) | ||
d67a15a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 12 | 2018-12-10T17:42:44+01:00 | ||
76f9055 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 13 | 2018-12-06T13:11:12+01:00 | ||
f68a0cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T20:34:48+01:00 | d67a15a | |
7dd8253 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T10:48:53+01:00 | dc44bd7 | |
e4d4295 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T21:23:40+01:00 | 909096f | |
d55a7fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:53:14+01:00 | 978b110 | |
3496c75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:34:17+01:00 | 89b41dd | |
9c60697 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:25:01+01:00 | 3ae9e26 | |
55d6658 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T18:21:52+01:00 | d7ecada | |
f13df3b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:44:01+01:00 | 31438ee | |
09153c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T22:09:58+01:00 | b7df11e | |
d565647 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T09:06:35+01:00 | 76f9055 | |
bb643ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T04:53:49+01:00 | fefe24c | |
f51a783 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T03:34:39+01:00 | dc44bd7 | |
30181fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T18:47:19+01:00 | 3992142 | |
bbf72df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T17:44:26+01:00 | 9cfebcd | |
fb1a5b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T01:06:31+01:00 | 9056911 | |
990552b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T10:19:59+01:00 | f4a7f12 | |
773a86c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:49:17+01:00 | 901ef54 | |
a424ce0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:19:56+01:00 | a16979d | |
901ef54 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-05T17:28:45+01:00 | ||
a1acbcb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:42:10+01:00 | 0391eb1 | |
d94a870 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:12:28+01:00 | 786368e | |
f943c3b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:12 CET (sv-comp) | ||
01c212e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:59 CET (sv-comp) |
Found 21 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c477473 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:38 CET (sv-comp) | ||
030367a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VIAP | 9 | 2017-12-03T03:57 CET (sv-comp) | ||
5a5e436 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 12 | 2017-12-03T00:12Z | ||
2fb99af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T11:06 CET (sv-comp) | ||
56aaefe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T21:22 CET (sv-comp) | ||
c4bb74a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 12 | 2017-12-02T19:16Z | ||
c030bd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T19:46:40.191789 | ||
066ac85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T08:03:22.220107 | ||
bf71e7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 6 | 2017-12-01T17:20 CET (sv-comp) | ||
41446bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 6 | 2017-12-01T05:26 CET (sv-comp) | ||
30ed78a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 12 | 2017-12-02T22:51:08+01:00 | ||
3432229 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 12 | 2017-11-30T16:28:35+01:00 | ||
14fa4ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 14 | 2017-12-01T00:46:44+01:00 | ||
6fcf356 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 9 | 2017-11-30T19:59:50+01:00 | ||
cff5760 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 8 | 2017-12-02T02:19:21+01:00 | ||
3e498c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 9 | 2017-11-30T23:28 CET (sv-comp) | ||
6dd9b15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 12 | 2017-12-02T17:49Z | ||
11f5b77 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 10 | 2017-11-30T13:18 CET (sv-comp) | ||
8555ae5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:11:57.185474 | ||
fde3a3d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T15:55:41.477813 | ||
485ca07 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 8 | 2017-12-01T19:05 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_false-unreach-call2_true-termination.i, 340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/340e7dc4e2cb041e942eaacf604ff71b4408ec46c9821378a0c92026bfa74466.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |