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_label26_true-unreach-call_false-termination.c |
programSHA | c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-termination.Problem01_label26_true-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | ff75d6419863a4e9588d1ce36dfbdd04d172e1fed9f4551767b24a12670a1ee4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T09:48:21+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c |
programhash | c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/ff75d6419863a4e9588d1ce36dfbdd04d172e1fed9f4551767b24a12670a1ee4.graphml |
witness-sha256 | ff75d6419863a4e9588d1ce36dfbdd04d172e1fed9f4551767b24a12670a1ee4 |
witness-size | 323849 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.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_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.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_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.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_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.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_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8c9de3d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T20:13:22+01:00 | 593d034 | |
1c437c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T20:02:31+01:00 | 918d8bb | |
4a2e9c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-08T00:50:16+01:00 | 482b991 | |
803e461 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T23:22:41+01:00 | 8bbcc31 | |
d377613 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T19:45:44+01:00 | 886df3e | |
48ff44d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T19:02:53+01:00 | 908a5e8 | |
33b52bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-11-30T17:10:54+01:00 | 7517081 | |
7517081 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 287 | 2019-11-30T13:04:03+01:00 | ||
593d034 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 287 | 2019-12-01T00:51:31+01:00 | ||
01836ae | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 339 | 2019-11-30T14:17:30+01:00 | ||
2bf8f35 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 339 | 2019-12-01T00:15:23+01:00 |
Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bcca7fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T09:20:28 | ||
5c2c5ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 287 | 2018-12-07T19:03:13+01:00 | ||
3f8fdf2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-10T20:04:14+01:00 | b2f5774 | |
816ef8d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:27:43+01:00 | 61f3a27 | |
de8376a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T17:28:53+01:00 | aba624a | |
248b98d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T21:49:21+01:00 | bcca7fc | |
8245d44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T07:15:00+01:00 | 5c2c5ea | |
ea87065 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T03:01:27+01:00 | 03640c9 | |
ea98025 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:28:28+01:00 | cad3983 | |
863d484 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:07:50+01:00 | 16b5ca4 | |
3832c17 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T07:30:36+01:00 | 9707b66 | |
16b5ca4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-05T14:14:30+01:00 | ||
d6525ff | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 339 | 2018-12-07T10:32:40+01:00 | ||
4b993bd | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-08T09:04:28+01:00 | ||
ff75d64 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 324 | 2018-12-06T09:48:21+01:00 | ||
1def189 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 327 | 2018-12-06T01:36:12+01:00 |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1de63a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 184 | 2017-12-02T05:54Z | ||
b530cef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
ec19c99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T04:07:55+01:00 | 1af22b2 | |
d5e80f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T02:56:57+01:00 | 9998e0b | |
ded160c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T00:35:26+01:00 | df96b19 | |
2120d13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-02T15:00:48+01:00 | 38a92fd | |
3c6742e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T07:18:08+01:00 | f144e6f | |
7c342b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T06:03:42+01:00 | a55b1c6 | |
cd335bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T05:41:43+01:00 | b743750 | |
57268bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T05:35:21+01:00 | b8fe55d | |
5069b1c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-11-30T18:05:55+01:00 | ||
2e3b1c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 469 | 2017-12-01T02:42:44+01:00 | ||
4a556c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 287 | 2017-11-30T20:42:37+01:00 | ||
92532d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 483 | 2017-12-02T08:51:38+01:00 | ||
d32ab78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 160 | 2017-12-02T02:06Z | ||
c83ecd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 778 | 2017-11-30T11:34 CET (sv-comp) | ||
38842b2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 315 | 2017-12-01T16:25:07+01:00 | ||
f9e8cf4 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 31 | 2017-12-01T12:55 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c, c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c04eeee213f55b39b463d4dc1a5f020e7588a625cf50d3b50b2c4d5f38341666.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |