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/systemc/transmitter.01_false-unreach-call_false-termination.cil.c |
programSHA | b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-divine-smt.2018-12-08_0324.logfiles/sv-comp19_prop-reachsafety.transmitter.01_false-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA | ec47cb6e48b9c35d093c53d34249871c48530302c80d8e18760dc1efb99a0f74 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T04:29:11+01:00 |
inputwitnesshash | c10e0b48b5c5d4f5fc4d6de5a1cd31f1b81011b737be09dfb8870e7049c7c261 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b |
programfile | ../../sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c |
programhash | b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/ec47cb6e48b9c35d093c53d34249871c48530302c80d8e18760dc1efb99a0f74.graphml |
witness-sha256 | ec47cb6e48b9c35d093c53d34249871c48530302c80d8e18760dc1efb99a0f74 |
witness-size | 44048 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b).
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 17 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
58bf0bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 02:30:17 | ||
fc8fc89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-11T21:57:13+01:00 | b021998 | |
234bd1c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-11T21:55:05+01:00 | 2e589c0 | |
94faa1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-11T21:09:01+01:00 | 58bf0bb | |
68ccd8c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 50 | 2019-12-11T20:55:01+01:00 | 4a0c1b8 | |
b76dd95 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-11T20:44:40+01:00 | f435db3 | |
75733d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-08T01:51:15+01:00 | b8f2c47 | |
bd807f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-08T00:26:02+01:00 | d0c11cd | |
c925b66 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-07T21:17:01+01:00 | 377a15e | |
14def68 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-03T08:57:39+01:00 | 5773615 | |
d759993 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-03T08:10:12+01:00 | 78e007a | |
78e007a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 40 | 2019-11-30T01:33:56+01:00 | ||
b8f2c47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 44 | 2019-12-07T15:10:35+01:00 | ||
b021998 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 42 | 2019-11-30T23:44:41+01:00 | ||
9c79069 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 36 | 2019-12-05T20:20:40+01:00 | 3de509b | |
5e078fa | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 114 | 2019-11-30T06:35:31+01:00 | ||
1175e08 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 114 | 2019-11-30T22:44:44+01:00 |
Found 21 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3b62d78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T12:48 CET (sv-comp) | ||
9889aa1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 9 | 2018-12-08T06:12:35 | ||
fae079a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 41 | 2018-12-07T06:47:35+01:00 | ||
7e891de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-09T20:53:12+01:00 | c89b812 | |
56a5be7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-09T20:37:26+01:00 | 915bb25 | |
c609be9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-09T20:33:48+01:00 | 6525852 | |
2c768a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-09T18:20:22+01:00 | 6844546 | |
d9728e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-08T23:43:54+01:00 | 3b62d78 | |
6c74366 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-08T22:10:19+01:00 | 9889aa1 | |
35c9d08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-08T08:56:19+01:00 | fae079a | |
db9728a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 50 | 2018-12-08T04:56:54+01:00 | a042b90 | |
ec47cb6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-08T04:29:11+01:00 | c10e0b4 | |
596da4f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 180 | 2018-12-06T10:15:09+01:00 | 1bf4276 | |
15422d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-06T09:49:03+01:00 | 1df0d47 | |
231f610 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-06T09:17:41+01:00 | 7e12050 | |
1df0d47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 41 | 2018-12-06T06:52:27+01:00 | ||
32b01d5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 37 | 2018-12-10T20:36:30+01:00 | 0e41a32 | |
c029f67 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 115 | 2018-12-08T02:45:22+01:00 | ||
d517a77 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-09T20:40:01+01:00 | ||
e3b0e70 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-06T10:20:00+01:00 | ||
b3d64a2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 115 | 2018-12-05T16:56:18+01:00 |
Found 15 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f3e05c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 54 | Sat Dec 2 18:44:16 2017 | ||
b06f9c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 56 | 2017-12-02T19:22Z | ||
eba3e9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T06:58 CET (sv-comp) | ||
d359281 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-01T18:43:57.581340 | ||
dedd571 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T08:22:10.351730 | ||
299c4aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 13 | 2017-12-01T15:24 CET (sv-comp) | ||
a929f45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 13 | 2017-12-01T00:12 CET (sv-comp) | ||
dda0e35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 37 | 2017-11-30T22:51:08+01:00 | ||
0f0c39a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 54 | 2017-12-01T00:11:27+01:00 | ||
f9ea0d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 31 | 2017-11-30T14:53:26+01:00 | ||
de9847a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 32 | 2017-12-02T11:53:03+01:00 | ||
fb0e390 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 22 | 2017-11-30T12:51 CET (sv-comp) | ||
d227830 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 56 | 2017-12-02T16:14Z | ||
a18ccfb | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 115 | 2017-12-01T12:27:17+01:00 | ||
94703df | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 31 | 2017-12-03T11:18Z |
Found 0 witnesses for program sv-benchmarks/c/systemc/transmitter.01_false-unreach-call_false-termination.cil.c, b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b1bfab0522dd9a036991ff135c15d92f8e748b1f2773b2c9ce4ea5c3938a1d8b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |