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/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c |
programSHA | c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-reachsafety.Problem02_label13_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 02b6a10bc93d9909a2cb9fbb7e719ce48e59a96c6de0fbdce42c979cbf718e3b |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T08:51:20+01:00 |
inputwitnesshash | c60ab5d82efe602918a49ebdb40d3db3c9824f2a38e66fa37f1b9c9d44e32fff |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c |
programhash | c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/02b6a10bc93d9909a2cb9fbb7e719ce48e59a96c6de0fbdce42c979cbf718e3b.graphml |
witness-sha256 | 02b6a10bc93d9909a2cb9fbb7e719ce48e59a96c6de0fbdce42c979cbf718e3b |
witness-size | 136067 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
38d6312 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 08:17:13 | ||
f5cd53c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 46 | 2019-12-04T00:43 CET (comp) | ||
5430cf3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 136 | 2019-12-11T21:56:33+01:00 | 58f3fd0 | |
92696a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 148 | 2019-12-11T21:51:17+01:00 | 734d97c | |
fd182b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 136 | 2019-12-11T21:09:22+01:00 | 38d6312 | |
a79fcaf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 136 | 2019-12-11T20:54:24+01:00 | 4e24e5f | |
224e641 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 136 | 2019-12-11T20:44:27+01:00 | b4e2add | |
efd2e37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 137 | 2019-12-08T01:52:38+01:00 | 0cec947 | |
a84b509 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 148 | 2019-12-08T00:27:19+01:00 | 0d33984 | |
e9f504d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 148 | 2019-12-07T21:18:28+01:00 | 81ba37c | |
ac7c9e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 167 | 2019-12-04T02:58:16+01:00 | f5cd53c | |
a94f808 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 136 | 2019-12-03T08:08:26+01:00 | 38ae3e8 | |
38ae3e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 135 | 2019-11-30T10:06:42+01:00 | ||
58f3fd0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 137 | 2019-12-01T19:30:12+01:00 | ||
3aad017 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T20:21:23+01:00 | cfaac9b | |
7b4d70d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T19:35:14+01:00 | fb97cbc | |
28a692d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 2 | 2019-12-01 11:05:23 | ||
1043849 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 359 | 2019-11-30T08:51:15+01:00 | ||
244f767 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 359 | 2019-12-01T13:12:49+01:00 |
Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d3f4df7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T16:59 CET (sv-comp) | ||
64ee951 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 6 | 2018-12-08T16:38:18 | ||
df51cf7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 53 | 2018-12-07T13:20 CET (sv-comp) | ||
c60ab5d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 137 | 2018-12-07T22:55:47+01:00 | ||
99b2b72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 137 | 2018-12-10T20:37:18+01:00 | 83e741b | |
e33cb19 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 148 | 2018-12-09T20:19:22+01:00 | a47d945 | |
7d5728b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 136 | 2018-12-09T18:21:17+01:00 | 2f68709 | |
2417230 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 137 | 2018-12-08T23:44:46+01:00 | d3f4df7 | |
6e25038 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 136 | 2018-12-08T22:11:30+01:00 | 64ee951 | |
02b6a10 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 136 | 2018-12-08T08:51:20+01:00 | c60ab5d | |
924e4a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 136 | 2018-12-08T05:05:38+01:00 | ec11b9f | |
6263e9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 167 | 2018-12-07T17:42:55+01:00 | df51cf7 | |
968182b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 136 | 2018-12-06T10:13:18+01:00 | 736369d | |
a2dc955 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 136 | 2018-12-06T09:49:08+01:00 | a9da05a | |
a9c8e9f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 290 | 2018-12-06T09:10:32+01:00 | 6b940a4 | |
a9da05a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 136 | 2018-12-05T16:14:06+01:00 | ||
6ee9ed0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:53:13+01:00 | 8c220f0 | |
3831700 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:35:35+01:00 | 30bdb08 | |
7cf78dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:43:58+01:00 | 46fb6fe | |
d516ae5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 359 | 2018-12-07T22:58:34+01:00 | ||
4d84f4f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-08T07:51:36+01:00 | ||
51d91d6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-06T09:48:56+01:00 | ||
e1c1f7a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 359 | 2018-12-05T14:44:49+01:00 |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4c5637a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-03T03:39 CET (sv-comp) | ||
9cef525 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 113 | 2017-12-03T05:20Z | ||
c6d7760 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T18:22 CET (sv-comp) | ||
64d9bbb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 113 | 2017-12-02T16:05Z | ||
f34eccd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T01:26:18.888241 | ||
2702845 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T12:54:46.920712 | ||
b6f8d59 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T18:33 CET (sv-comp) | ||
4756039 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-11-30T20:31 CET (sv-comp) | ||
36e7ad0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 77 | 2017-12-01T01:38:39+01:00 | ||
3434305 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 172 | 2017-12-01T01:25:50+01:00 | ||
e7cc888 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 74 | 2017-11-30T17:57:23+01:00 | ||
67c4101 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 104 | 2017-12-02T09:48:25+01:00 | ||
19e3526 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 98 | 2017-11-30T11:50 CET (sv-comp) | ||
98b43a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 113 | 2017-12-02T09:11Z | ||
857d31f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 59 | 2017-11-30T20:33 CET (sv-comp) | ||
98acba9 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 334 | 2017-12-01T13:44:09+01:00 | ||
7e2be37 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 15 | 2017-12-03T11:18Z | ||
8a63876 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T15:57 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c, c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c73c00e3f5a4f316da06f3249b7e90206564c4c24fe22d4fa4376b18dc832827.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |