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/Problem01_label21_false-unreach-call_false-termination.c |
programSHA | e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-utaipan.2018-12-09_2052.logfiles/sv-comp19_prop-reachsafety.Problem01_label21_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | ab883ff55e18f562d5e57a05f8cfb4956cc821dba5a6952eb3479ba18b6c65df |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T20:53:28+01:00 |
inputwitnesshash | 7b875fa62a81811042d91b2044996112a59e84d85cbe6578be4bfbe202a19fed |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c |
programhash | e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/ab883ff55e18f562d5e57a05f8cfb4956cc821dba5a6952eb3479ba18b6c65df.graphml |
witness-sha256 | ab883ff55e18f562d5e57a05f8cfb4956cc821dba5a6952eb3479ba18b6c65df |
witness-size | 287413 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.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/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.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/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.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/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
54de9a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 21:07:37 | ||
2fd59b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 67 | 2019-12-03T22:46 CET (comp) | ||
3d8e1d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 201 | 2019-12-11T21:43:18+01:00 | b93bd61 | |
12d5ebb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 201 | 2019-12-11T21:09:32+01:00 | 54de9a8 | |
fb32afd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 201 | 2019-12-11T20:54:23+01:00 | aae9bf9 | |
d37b40d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 201 | 2019-12-11T20:44:33+01:00 | 3faa055 | |
7073d31 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 202 | 2019-12-08T01:51:39+01:00 | 1aea219 | |
6842b75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 253 | 2019-12-04T03:00:00+01:00 | 2fd59b0 | |
4219013 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 201 | 2019-12-03T08:08:58+01:00 | 8f1c7d6 | |
8f1c7d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 200 | 2019-11-29T14:52:45+01:00 | ||
b93bd61 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 201 | 2019-11-30T22:52:48+01:00 | ||
3c0a60c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T22:00:26+01:00 | 449db8d | |
1bac80a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-08T00:27:50+01:00 | 6af54a1 | |
9c9fa7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T21:18:50+01:00 | 45e6b4f | |
2d0d7ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T20:22:37+01:00 | bb8431e | |
46fb193 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T19:35:29+01:00 | bc21983 | |
37734ee | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 339 | 2019-11-29T14:13:07+01:00 | ||
89758c5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 339 | 2019-12-01T09:35:52+01:00 |
Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ef8e4f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-07T22:52 CET (sv-comp) | ||
effd9a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 8 | 2018-12-08T12:51:40 | ||
82265e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 78 | 2018-12-07T09:18 CET (sv-comp) | ||
ab3b1f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 201 | 2018-12-07T04:26:56+01:00 | ||
41dfe00 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 202 | 2018-12-10T20:37:01+01:00 | 2c9dc5c | |
9971c79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-09T18:21:58+01:00 | 2e3e526 | |
f46b4ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T23:44:50+01:00 | ef8e4f5 | |
a952301 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-08T22:10:56+01:00 | effd9a5 | |
d53269d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-08T08:10:27+01:00 | ab3b1f4 | |
67c919a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-08T05:05:23+01:00 | 7c6f114 | |
6ab3eab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 253 | 2018-12-07T17:44:51+01:00 | 82265e3 | |
bb72993 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-06T10:19:26+01:00 | 9d65d41 | |
ba1a71d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-06T09:48:16+01:00 | a4d76c0 | |
4f51976 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 254 | 2018-12-06T09:18:30+01:00 | f92b71a | |
a4d76c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 200 | 2018-12-05T09:24:50+01:00 | ||
ab883ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:53:28+01:00 | 7b875fa | |
d2ef337 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:35:51+01:00 | edc6802 | |
28db3f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:18:26+01:00 | 4078342 | |
a70d7ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:43:41+01:00 | d2e13b1 | |
6fced82 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 339 | 2018-12-07T22:59:33+01:00 | ||
8755d30 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-08T08:59:35+01:00 | ||
15392a4 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 324 | 2018-12-06T09:49:09+01:00 | ||
bf45747 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 327 | 2018-12-05T15:26:40+01:00 |
Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c58de39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-02T22:09 CET (sv-comp) | ||
850735c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T16:16 CET (sv-comp) | ||
e7f85d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 172 | 2017-12-02T17:17Z | ||
dd4008a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-01T21:43:52.869022 | ||
401feee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T13:02:30.318411 | ||
f27fc0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 13 | 2017-12-01T16:47 CET (sv-comp) | ||
9ec055d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 13 | 2017-12-01T04:38 CET (sv-comp) | ||
2962b19 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 114 | 2017-11-30T15:35:09+01:00 | ||
b907c96 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 288 | 2017-11-30T18:52:39+01:00 | ||
e9358ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 110 | 2017-12-01T02:58:34+01:00 | ||
9c80f45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 179 | 2017-12-01T22:29:01+01:00 | ||
4b87594 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 86 | 2017-11-30T23:47 CET (sv-comp) | ||
9ab5faf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 172 | 2017-12-02T16:23Z | ||
3687d45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 87 | 2017-11-30T17:07 CET (sv-comp) | ||
52749ea | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 31 | 2017-12-01T13:48 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c, e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e7342ebe8cad3814252ee44bb7c094efa1029743dfb8aa628b7958247a63cfe2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |