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/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i |
programSHA | f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc |
witnessName | results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.SpamAssassin-loop_true-unreach-call_false-termination.i.files/witness.graphml |
witnessSHA | 1284ef40ae1e91e9c03c57371ed5a3d0fd83fb20b3f0d1885c3c1b7f876666ad |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T17:51:43+01:00 |
producer | CPAchecker 1.7-svn b8d6131600+ |
program-sha256 | f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc |
programfile | ../../sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i |
programhash | f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/1284ef40ae1e91e9c03c57371ed5a3d0fd83fb20b3f0d1885c3c1b7f876666ad.graphml |
witness-sha256 | 1284ef40ae1e91e9c03c57371ed5a3d0fd83fb20b3f0d1885c3c1b7f876666ad |
witness-size | 14877 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc).
Found 0 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 10 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
93d874a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T20:23:34+01:00 | 41e193c | |
6041774 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-08T00:36:36+01:00 | 820d883 | |
b32bcaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-07T23:32:27+01:00 | 711b2b0 | |
faa69ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-07T19:44:36+01:00 | 486e883 | |
6b4b174 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-05T19:03:04+01:00 | dc7f9d5 | |
d2d3d31 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-11-30T17:22:09+01:00 | 8556b72 | |
8556b72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 15 | 2019-11-30T04:09:58+01:00 | ||
820d883 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 15 | 2019-12-07T22:11:01+01:00 | ||
07c8465 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 25 | 2019-11-30T04:04:02+01:00 | ||
00488d7 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 25 | 2019-12-01T02:00:04+01:00 |
Found 13 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1284ef4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-07T17:51:43+01:00 | ||
cc16583 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-10T19:56:11+01:00 | bd14425 | |
747515f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:32:23+01:00 | ab4893c | |
8224d9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:21:32+01:00 | b4520ad | |
428ed63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:08:21+01:00 | 5dfd8c6 | |
9466d9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T07:32:55+01:00 | 1284ef4 | |
eaae048 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T09:26:49+01:00 | 9a5ef03 | |
067de85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T08:02:17+01:00 | 1474813 | |
9a5ef03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T02:23:17+01:00 | ||
9d04fc7 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 25 | 2018-12-07T10:12:03+01:00 | ||
2520a57 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-09T20:40:08+01:00 | ||
0ae9424 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-06T09:42:13+01:00 | ||
b15807b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-05T15:49:19+01:00 |
Found 21 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e411427 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 20 | 2017-12-03T05:08Z | ||
9f5037a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 21 | 2017-12-02T06:02Z | ||
c68f204 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 15 | 2017-12-02T21:13:29+01:00 | ||
7b9cfcb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-03T07:05:00+01:00 | 0c531d5 | |
36c8ad0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-03T04:41:28+01:00 | 024a403 | |
09d92f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-03T01:09:49+01:00 | df1a63e | |
53e6d0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-02T23:54:28+01:00 | c365816 | |
a45ead6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-02T15:25:21+01:00 | 91c4805 | |
4751139 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T07:06:14+01:00 | 5119147 | |
ca4ade3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T06:02:31+01:00 | 3c77a1a | |
dd1b798 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T05:51:15+01:00 | 1dcc5a9 | |
ce83583 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T05:41:52+01:00 | e99d038 | |
55b36a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-11-30T21:52:49+01:00 | ||
0ae34d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 9 | 2017-11-30T20:18:23+01:00 | ||
16b1590 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 15 | 2017-11-30T13:17:26+01:00 | ||
e9c769f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 14 | 2017-12-02T06:47:42+01:00 | ||
6f6efea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 19 | 2017-12-02T17:34Z | ||
2d30c92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 298 | 2017-11-30T15:18 CET (sv-comp) | ||
e98ac93 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T15:10:18+01:00 | ||
8867cba | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 7 | 2017-12-03T11:13Z | ||
9e5879d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 6 | 2017-12-01T12:17 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i, f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f36a6f7a32113ae02d2de1e52f83c18ccb2063a0868547db452822ab1ed650bc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |