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_label36_true-unreach-call_false-termination.c |
programSHA | ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7 |
witnessName | results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-termination.Problem01_label36_true-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | d0c975379b921a7e7715d890f583a86969d40caafa131d8fedee17cdf2fb4170 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T13:03:16+01:00 |
producer | CPAchecker 1.7-svn b8d6131600+ |
program-sha256 | ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c |
programhash | ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/d0c975379b921a7e7715d890f583a86969d40caafa131d8fedee17cdf2fb4170.graphml |
witness-sha256 | d0c975379b921a7e7715d890f583a86969d40caafa131d8fedee17cdf2fb4170 |
witness-size | 338807 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.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_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.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_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.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_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4128da7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T20:07:13+01:00 | 520d9ab | |
6c500a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T20:03:04+01:00 | cde81bb | |
c42cae9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-08T00:36:32+01:00 | 91bdc43 | |
09fed97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T23:44:46+01:00 | 718ef13 | |
96be195 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T19:47:49+01:00 | 5f030cf | |
2bbd01e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T19:03:08+01:00 | 95f77dd | |
f95bba8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-11-30T17:28:36+01:00 | 6ce2f2b | |
6ce2f2b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 287 | 2019-11-29T14:55:25+01:00 | ||
520d9ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 287 | 2019-12-01T01:47:06+01:00 | ||
a1d167b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 339 | 2019-11-29T14:57:51+01:00 | ||
0650bc5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 339 | 2019-12-01T10:50:33+01:00 |
Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
047977f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T02:15:14 | ||
123fd48 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 287 | 2018-12-07T09:56:45+01:00 | ||
bc83704 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-10T19:39:55+01:00 | a1472a1 | |
bcf3601 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:27:57+01:00 | 15b53f8 | |
80b012c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T17:13:41+01:00 | 1d9ef0e | |
be65620 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T21:44:18+01:00 | 047977f | |
43b23c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T05:29:02+01:00 | 123fd48 | |
fcd80f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T03:58:03+01:00 | dafae2c | |
7572ab2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:28:36+01:00 | 90b10b9 | |
8c090a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T08:45:40+01:00 | 8b958dc | |
785a4b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T07:51:45+01:00 | 8f84d15 | |
8b958dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-05T21:41:35+01:00 | ||
d0c9753 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 339 | 2018-12-06T13:03:16+01:00 | ||
de8be61 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-08T08:48:38+01:00 | ||
dd6bc9b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 324 | 2018-12-06T09:48:01+01:00 | ||
c30e6b9 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 327 | 2018-12-05T15:37:57+01:00 |
Found 20 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b25b24c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 160 | 2017-12-03T03:05Z | ||
2596bc2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 174 | 2017-12-02T19:00Z | ||
da70a74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
0ae7438 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T06:52:39+01:00 | 0365628 | |
99f133e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T04:12:13+01:00 | 58dde47 | |
41b365d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T02:31:17+01:00 | 8f189c2 | |
914580c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 291 | 2017-12-03T01:33:29+01:00 | 6d0852e | |
e06f08d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-02T14:53:54+01:00 | a3ea11d | |
c9b4133 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T07:00:01+01:00 | fd479e4 | |
2b02f7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T06:45:33+01:00 | 1662fd1 | |
34ae068 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T06:17:56+01:00 | 7628562 | |
0a7eb79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T06:11:43+01:00 | ae91fd6 | |
8db5be4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T03:12:30+01:00 | ||
2745b42 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 510 | 2017-11-30T23:59:32+01:00 | ||
b199974 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 287 | 2017-11-30T23:57:24+01:00 | ||
2c1c9c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 504 | 2017-12-02T10:34:44+01:00 | ||
e03fad4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 160 | 2017-12-02T05:18Z | ||
c4c774e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 778 | 2017-11-30T15:43 CET (sv-comp) | ||
47ddc15 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 315 | 2017-12-01T15:39:23+01:00 | ||
4f0a92a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 31 | 2017-12-01T14:15 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c, ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ddecd0264e34830081737a8b701c31cc3427047082af25cd014f5adb18532fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |