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/string_true-unreach-call_true-termination.i |
programSHA | fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174 |
witnessName | results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-reachsafety.string_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 |
Key | Value |
creationtime | 2018-12-05T13:03 CET (sv-comp) |
error-programhash | Key 'programhash' not present. |
error-specification-exists | Key 'specification' not present. |
error-xmlparsing | File produces XML parsing error. |
witness-file | witnessFileByHash/e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855.graphml |
witness-sha256 | e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 |
witness-size | 0 |
The following keys are missing in the witness XML file: witness-type, sourcecodelang, producer, specification, programfile, programhash, architecture.
Found 0 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 17 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
64b4eca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:25 CET (comp) | ||
e296a0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:30:59+01:00 | 99f0660 | |
3b086aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:12:27+01:00 | 1dcd678 | |
c82109e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:12:06+01:00 | 5bca711 | |
c875626 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:02:27+01:00 | 23f6d12 | |
f926a56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-08T00:41:38+01:00 | e14864d | |
f102ed3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T23:32:23+01:00 | f2e4b37 | |
7323d79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T19:41:15+01:00 | ab5c814 | |
a20a0f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-06T02:14:54+01:00 | e8c4287 | |
6dd2060 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T19:12:52+01:00 | 6f3e570 | |
d01c783 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T19:03:00+01:00 | 464a893 | |
ef12533 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-04T02:07:52+01:00 | 64b4eca | |
575fd4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-11-30T19:56:17+01:00 | 70bbe89 | |
d5edbc9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-11-30T16:34:20+01:00 | d20139c | |
d20139c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 14 | 2019-11-30T04:14:36+01:00 | ||
5bca711 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 13 | 2019-12-01T11:09:13+01:00 | ||
4ebec02 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:48 CET (comp) |
Found 22 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
771eaeb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:39 CET (sv-comp) | ||
96fdba9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T13:38:25 | ||
86decbc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T09:01 CET (sv-comp) | ||
28ba520 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 17 | 2018-12-07T05:27:39+01:00 | ||
a878c2b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T20:07:17+01:00 | 92781c8 | |
bfd04cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:27:39+01:00 | 8f4b2c3 | |
48d4bd7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T19:49:16+01:00 | 5fb9d64 | |
deddacc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T17:27:50+01:00 | f1d1907 | |
9ca3db0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:11:23+01:00 | 771eaeb | |
71a5ea9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T21:29:30+01:00 | 96fdba9 | |
0f94ae0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T06:29:46+01:00 | 28ba520 | |
3d268f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T04:18:57+01:00 | 3c87ab4 | |
46722d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T02:27:33+01:00 | 37b508f | |
b1d172b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T17:45:24+01:00 | 2d56399 | |
16a7b1a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T16:37:47+01:00 | 86decbc | |
d857dee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:29:06+01:00 | 7bb2a82 | |
8295970 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:05:34+01:00 | 101ffc8 | |
f6d94ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T07:58:30+01:00 | c17a4e5 | |
f984074 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T07:22:59+01:00 | 820f061 | |
101ffc8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T02:51:50+01:00 | ||
1c2befb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T19:16 CET (sv-comp) | ||
c6e2b3c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T12:07 CET (sv-comp) |
Found 34 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2d56399 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:04 CET (sv-comp) | ||
75515ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 14 | 2017-12-03T02:58Z | ||
c472510 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-01T23:48 CET (sv-comp) | ||
5a74dd5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 6 | 2017-12-01T20:13 CET (sv-comp) | ||
3fe4168 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 13 | 2017-12-02T08:21Z | ||
ecdc209 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:36:44.038088 | ||
8d1f6c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T11:41:56.356765 | ||
febadb5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T17:35:26.728151 | ||
7115d53 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T15:54:43.532490 | ||
f6b2878 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 13 | 2017-12-01T17:45 CET (sv-comp) | ||
da7b1c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
794b11a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T17:30:42+01:00 | ||
5844894 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-03T06:50:44+01:00 | 3af1a6e | |
36ac1ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-03T04:18:34+01:00 | 7e5732a | |
09ba37b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 16 | 2017-12-03T01:06:56+01:00 | d79e4c2 | |
d7b785c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-02T23:32:29+01:00 | 602da3a | |
192d71e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T19:52:52+01:00 | 2a414ff | |
47cd1f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T08:01:37+01:00 | c97446f | |
8aafb81 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T00:04:49+01:00 | 40402f0 | |
b129b57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T22:21:39+01:00 | ce86b30 | |
e4446fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T22:12:26+01:00 | 94933a9 | |
e794832 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T08:14:06+01:00 | b7909f1 | |
518de71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-01T07:18:55+01:00 | 0df8af7 | |
ad6717e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T07:15:54+01:00 | b35fcce | |
306f5ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T06:59:14+01:00 | efbd5af | |
e4a8917 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-01T06:45:19+01:00 | d9050db | |
6ce8ad1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T05:34:34+01:00 | 8822f42 | |
2c97fed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-11-30T12:50:08+01:00 | ||
1096953 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 9 | 2017-11-30T14:06:38+01:00 | ||
c787ffe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 13 | 2017-11-30T16:35:08+01:00 | ||
6ed802d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 49 | 2017-12-01T03:33 CET (sv-comp) | ||
aae104a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 13 | 2017-12-02T15:04Z | ||
13906f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 24 | 2017-12-01T02:26 CET (sv-comp) | ||
6646d7e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 49 | 2017-12-01T16:10 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/string_true-unreach-call_true-termination.i, fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/fee8c566104c383a399051f03161e995b7793642fba144cd880baaed2c4f2174.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |