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_label48_true-unreach-call_false-termination.c |
programSHA | b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045 |
witnessName | results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-termination.Problem01_label48_true-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | bc8f89398489782a7956f77862a540e70aa1eac7bb9c77b0e1afcdcf6e0e1d55 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T11:10 CET (sv-comp) |
producer | 2LS |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c |
programhash | 0efda15f8357629016064e69e444205aff537305 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/bc8f89398489782a7956f77862a540e70aa1eac7bb9c77b0e1afcdcf6e0e1d55.graphml |
witness-sha256 | bc8f89398489782a7956f77862a540e70aa1eac7bb9c77b0e1afcdcf6e0e1d55 |
witness-size | 42493 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.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_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.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_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.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_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.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_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3bafbcd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T20:07:11+01:00 | fe45bd7 | |
1f3bc7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T20:02:29+01:00 | 50e897e | |
82450bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-08T00:59:45+01:00 | 6864e9c | |
3df04d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T23:44:13+01:00 | 0837906 | |
8f88e06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T19:41:01+01:00 | 70bc63a | |
ebfb7fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T19:02:58+01:00 | ba22254 | |
278bfe1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-11-30T16:43:27+01:00 | 6d7e9db | |
6d7e9db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 287 | 2019-11-29T15:27:51+01:00 | ||
fe45bd7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 287 | 2019-11-30T20:43:27+01:00 | ||
a60832e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 339 | 2019-11-29T23:03:52+01:00 | ||
f54d791 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 339 | 2019-11-30T20:30:06+01:00 |
Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e9db7b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:18:10 | ||
c319571 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 287 | 2018-12-08T04:05:59+01:00 | ||
3c680e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-10T19:55:58+01:00 | b6a373e | |
a97b752 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:33:57+01:00 | 409c93f | |
222528c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:03:34+01:00 | de03608 | |
e698dca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T21:40:10+01:00 | e9db7b7 | |
f462afb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T05:30:06+01:00 | c319571 | |
5d93191 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-08T03:27:43+01:00 | 7a3cda0 | |
84d5ff4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:28:30+01:00 | ef0c4dc | |
a3ea810 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:08:12+01:00 | 737c61b | |
2ced230 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T07:57:23+01:00 | 392585e | |
737c61b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-05T16:56:34+01:00 | ||
e2c2708 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 339 | 2018-12-07T06:33:21+01:00 | ||
4c6cae2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-08T09:02:44+01:00 | ||
bb741d4 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 324 | 2018-12-06T09:48:03+01:00 | ||
4c4f764 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 327 | 2018-12-06T00:10:21+01:00 |
Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
901d4ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 160 | 2017-12-03T05:11Z | ||
9b8dc68 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 179 | 2017-12-02T01:58Z | ||
9a3baa2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
be11523 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T06:50:44+01:00 | d81c9cb | |
4c025c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T04:27:05+01:00 | 38ddbad | |
60f05c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 293 | 2017-12-03T02:49:57+01:00 | d96b885 | |
530280a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-03T02:06:35+01:00 | 80155ef | |
c5ae98b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-02T15:22:29+01:00 | d291972 | |
4eab8e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T07:14:06+01:00 | ae48d03 | |
e6be103 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T07:13:06+01:00 | 416b281 | |
2af7a17 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T05:35:48+01:00 | bc4afbf | |
6962da1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-12-01T05:06:33+01:00 | eb89fa3 | |
1ee2867 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 287 | 2017-11-30T14:03:14+01:00 | ||
a2749a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 510 | 2017-11-30T14:35:31+01:00 | ||
f37d1d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 287 | 2017-11-30T14:39:36+01:00 | ||
2a6d738 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 504 | 2017-12-02T12:37:07+01:00 | ||
e588829 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 160 | 2017-12-02T17:13Z | ||
bdb6c7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 778 | 2017-11-30T16:34 CET (sv-comp) | ||
b8b8413 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 31 | 2017-12-01T12:27 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c, b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b91a2dd660a9352b83ac94a4af4d94b5a967df6e46451f06909ba78b56c2f045.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |