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_label44_false-unreach-call_false-termination.c |
programSHA | 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d |
witnessName | results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.Problem01_label44_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | cfc5343f9f7088d150cab424312984205cd4f83c9711d636fa29d31100b5cd55 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T02:57Z |
producer | Kojak |
program-sha256 | 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_515f5135-cb52-4c39-8417-cfbcf08f1dea/sv-benchmarks/c/eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c |
programhash | 2239efb232e6960cd140d60028ed9446da6b2730 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/cfc5343f9f7088d150cab424312984205cd4f83c9711d636fa29d31100b5cd55.graphml |
witness-sha256 | cfc5343f9f7088d150cab424312984205cd4f83c9711d636fa29d31100b5cd55 |
witness-size | 121371 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.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_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.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_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.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_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.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_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a1d12c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 12:57:45 | ||
1db7fe9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 47 | 2019-12-03T22:38 CET (comp) | ||
ea18bf3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 249 | 2019-12-11T21:46:13+01:00 | f03b06b | |
9eca939 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 143 | 2019-12-11T21:41:09+01:00 | 3629633 | |
60c541d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 143 | 2019-12-11T21:09:24+01:00 | a1d12c9 | |
8d70a2f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 192 | 2019-12-11T20:54:50+01:00 | 7938bbb | |
52aee3b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 143 | 2019-12-11T20:44:54+01:00 | 72706be | |
269eb0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 144 | 2019-12-08T01:51:41+01:00 | 47e3f14 | |
dd62b3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 249 | 2019-12-08T00:33:54+01:00 | 8528a79 | |
06ccd0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 249 | 2019-12-07T21:13:29+01:00 | 8127895 | |
47fdd63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 182 | 2019-12-04T02:58:21+01:00 | 1db7fe9 | |
71ae25e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 143 | 2019-12-03T08:10:32+01:00 | 8d5805d | |
8d5805d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 141 | 2019-11-30T11:36:26+01:00 | ||
3629633 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 142 | 2019-12-01T15:19:15+01:00 | ||
dff2f14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T20:21:50+01:00 | 187b0c8 | |
6a90443 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T19:35:39+01:00 | 725900a | |
250edfd | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 339 | 2019-11-29T15:44:58+01:00 | ||
f83d5ab | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 339 | 2019-12-01T16:38:12+01:00 |
Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9ee0077 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:53 CET (sv-comp) | ||
4af396f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 6 | 2018-12-08T12:23:05 | ||
86c65ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 55 | 2018-12-06T20:53 CET (sv-comp) | ||
945e38d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 143 | 2018-12-07T00:18:25+01:00 | ||
ce2305c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 144 | 2018-12-10T20:37:53+01:00 | 119fa55 | |
dc1c458 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 249 | 2018-12-09T20:26:01+01:00 | 02e040c | |
e5325c3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 143 | 2018-12-09T18:12:53+01:00 | 5726029 | |
ae10a30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 144 | 2018-12-08T23:43:49+01:00 | 9ee0077 | |
224ce9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 143 | 2018-12-08T22:08:36+01:00 | 4af396f | |
968a5d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 143 | 2018-12-08T07:59:34+01:00 | 945e38d | |
400556b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 190 | 2018-12-08T05:04:57+01:00 | fb1fe04 | |
a3ccc27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 182 | 2018-12-07T17:44:42+01:00 | 86c65ed | |
2f6cf37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 143 | 2018-12-06T10:19:58+01:00 | 6970870 | |
b6551a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 143 | 2018-12-06T09:48:17+01:00 | bd6ef92 | |
0b85f55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 244 | 2018-12-06T09:18:11+01:00 | 05ac11e | |
bd6ef92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 141 | 2018-12-05T16:34:25+01:00 | ||
12311c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:53:23+01:00 | d3de8d0 | |
59a9049 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:34:14+01:00 | 4819f67 | |
2fcb42e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:42:35+01:00 | 7bd4d13 | |
ed18e5a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 339 | 2018-12-08T03:29:56+01:00 | ||
2adcbda | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-08T08:13:25+01:00 | ||
e429a83 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 324 | 2018-12-06T09:48:48+01:00 | ||
b49d0cc | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 327 | 2018-12-05T20:10:15+01:00 |
Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d5c6246 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-03T03:07 CET (sv-comp) | ||
64a8c2b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 122 | 2017-12-03T05:20Z | ||
884be6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T12:27 CET (sv-comp) | ||
cfc5343 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 121 | 2017-12-02T02:57Z | ||
3b687b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T19:07:33.259214 | ||
7f88943 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T18:53:04.212583 | ||
ca75863 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T19:26 CET (sv-comp) | ||
6b4f30e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T03:41 CET (sv-comp) | ||
cbb5c71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 82 | 2017-11-30T20:36:59+01:00 | ||
9f53509 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 205 | 2017-11-30T13:43:20+01:00 | ||
e0ced78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 87 | 2017-11-30T23:30:52+01:00 | ||
e4a67e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 79 | 2017-11-30T13:18 CET (sv-comp) | ||
e80d62c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 122 | 2017-12-02T18:04Z | ||
cb1b034 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 60 | 2017-11-30T14:26 CET (sv-comp) | ||
5b1117c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 31 | 2017-12-01T14:13 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c, 6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6770b4c861cd7373c31682afbb3c485894806b45c2141e4523919ca97c0f3c7d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |