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/Problem03_label27_false-unreach-call.c |
programSHA | 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a |
witnessName | results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.Problem03_label27_false-unreach-call.c.files/witness.graphml |
witnessSHA | 4955ba39a5cd5008d0f5dae3821cdc6f015e0018fc928050091dcdad314b383d |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T05:04:45+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c |
programhash | 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/4955ba39a5cd5008d0f5dae3821cdc6f015e0018fc928050091dcdad314b383d.graphml |
witness-sha256 | 4955ba39a5cd5008d0f5dae3821cdc6f015e0018fc928050091dcdad314b383d |
witness-size | 390440 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.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/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.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/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.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/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6353eb1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 08:35:14 | ||
e4a663c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 117 | 2019-12-03T22:21 CET (comp) | ||
7d0ffb3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 390 | 2019-12-11T21:41:19+01:00 | 1370e65 | |
38494fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 390 | 2019-12-11T21:09:37+01:00 | 6353eb1 | |
f1bf77a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 390 | 2019-12-11T20:54:49+01:00 | 872e57c | |
cf5aff9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 390 | 2019-12-11T20:44:30+01:00 | 394b040 | |
8a0b3b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 391 | 2019-12-08T01:52:26+01:00 | be52c73 | |
9c224db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 518 | 2019-12-04T02:58:19+01:00 | e4a663c | |
5173b8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 390 | 2019-12-03T08:08:51+01:00 | aaae5e4 | |
aaae5e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 390 | 2019-11-30T14:51:25+01:00 | ||
1370e65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 390 | 2019-12-01T17:55:31+01:00 | ||
6afa3dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 685 | 2019-12-07T21:14:13+01:00 | 2321e4f |
Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4de3834 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T10:10 CET (sv-comp) | ||
acd413f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 11 | 2018-12-08T03:48:05 | ||
8a9969f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 127 | 2018-12-07T10:34 CET (sv-comp) | ||
4abc341 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 394 | 2018-12-07T23:14:35+01:00 | ||
dfd7038 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 391 | 2018-12-10T20:38:02+01:00 | 14be678 | |
4b84823 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 390 | 2018-12-09T18:21:35+01:00 | 5548683 | |
87b8475 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 393 | 2018-12-08T23:44:07+01:00 | 4de3834 | |
d435a22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 390 | 2018-12-08T22:10:35+01:00 | acd413f | |
222e3d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 390 | 2018-12-08T08:05:17+01:00 | 4abc341 | |
210e882 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 390 | 2018-12-08T05:01:49+01:00 | b3e6422 | |
965ff6a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 518 | 2018-12-07T17:43:18+01:00 | 8a9969f | |
92a0f3b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 390 | 2018-12-06T10:18:13+01:00 | c6d1c55 | |
ba76f22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 390 | 2018-12-06T09:48:55+01:00 | 4955ba3 | |
ef08a78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 518 | 2018-12-06T09:20:07+01:00 | 830ddba | |
4955ba3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 390 | 2018-12-06T05:04:45+01:00 | ||
ade1af7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 685 | 2018-12-09T20:54:34+01:00 | e1c5b6e |
Found 9 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5762904 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-02T22:55 CET (sv-comp) | ||
8b0f477 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T06:13 CET (sv-comp) | ||
18adfe2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-01T12:40:42.702609 | ||
3c5389b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T12:04:06.452187 | ||
14a0381 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 19 | 2017-12-01T00:32 CET (sv-comp) | ||
381b08e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 223 | 2017-11-30T18:00:55+01:00 | ||
9d3ee3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 833 | 2017-12-01T00:05:25+01:00 | ||
1bc95fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 144 | 2017-11-30T12:23 CET (sv-comp) | ||
ab12923 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 145 | 2017-11-30T19:08 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |