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/pc_sfifo_2_false-unreach-call_false-termination.cil.c |
programSHA | 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232 |
witnessName | results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.pc_sfifo_2_false-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA | e00cb76192c0097475a9b886873b85d2e2356923cbfef054e246f5a30673008f |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T08:20:27.657807 |
producer | ESBMC 4.6.0 incr |
program-sha256 | 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232 |
programfile | ../../sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c |
programhash | df684da5e5a56662a7be6091ec5bb0a21e1453c5 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/e00cb76192c0097475a9b886873b85d2e2356923cbfef054e246f5a30673008f.graphml |
witness-sha256 | e00cb76192c0097475a9b886873b85d2e2356923cbfef054e246f5a30673008f |
witness-size | 3808 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 14 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d4bec0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 01:59:03 | ||
6c4f232 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 16 | 2019-12-03T21:44 CET (comp) | ||
7a8f834 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-11T21:54:45+01:00 | c384a1c | |
f2512b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-11T21:09:38+01:00 | d4bec0d | |
5f116ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-11T20:54:27+01:00 | 7d67ce8 | |
27a5a76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 1653 | 2019-12-11T20:44:36+01:00 | 51ed713 | |
9513508 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-08T00:27:18+01:00 | d6e9c3d | |
65b6714 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-07T21:18:03+01:00 | 216fa2b | |
82856f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-05T20:21:25+01:00 | cb14e04 | |
32e2b04 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-04T02:58:04+01:00 | 6c4f232 | |
245795b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-03T08:56:47+01:00 | efaa454 | |
2f67b6b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-03T08:09:45+01:00 | f7f0014 | |
f7f0014 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 22 | 2019-11-29T15:53:08+01:00 | ||
c384a1c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 22 | 2019-12-01T05:07:49+01:00 |
Found 16 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2bd728a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T08:58 CET (sv-comp) | ||
90044b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 7 | 2018-12-08T14:27:12 | ||
95cfc0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 23 | 2018-12-07T18:02:52+01:00 | ||
00bfac5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-09T20:53:09+01:00 | 418431e | |
d25c8e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-09T20:36:35+01:00 | 65e7cab | |
dad3f1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-09T18:21:54+01:00 | fd2056d | |
d797ff9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-08T23:41:55+01:00 | 2bd728a | |
dac041e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-08T22:08:49+01:00 | 90044b7 | |
139350b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-08T08:45:03+01:00 | 95cfc0b | |
142fbd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-08T04:59:16+01:00 | bff2b6b | |
2cf6eed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-08T03:33:33+01:00 | 3e09513 | |
dd302e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T10:10:32+01:00 | 405a3a7 | |
c7dcb71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T09:48:53+01:00 | a4e9057 | |
281edc8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T09:19:13+01:00 | 339559f | |
1e82bb7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T09:18:13+01:00 | f426df4 | |
a4e9057 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T03:41:10+01:00 |
Found 15 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a4dd692 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 13 | Sun Dec 3 00:11:05 2017 | ||
431fcd3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 36 | 2017-12-02T22:46Z | ||
48d5732 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T02:38 CET (sv-comp) | ||
cb90c09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 36 | 2017-12-02T12:10Z | ||
5a0aa9f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T03:01:50.326348 | ||
e00cb76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T08:20:27.657807 | ||
6c5f2e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 11 | 2017-12-01T20:05 CET (sv-comp) | ||
f865d1b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 11 | 2017-12-01T04:14 CET (sv-comp) | ||
30c821e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-11-30T14:25:27+01:00 | ||
7c1d858 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 39 | 2017-11-30T11:35:29+01:00 | ||
33a224e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 17 | 2017-11-30T15:50:11+01:00 | ||
f962cf9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 17 | 2017-12-01T19:30:52+01:00 | ||
2242372 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 36 | 2017-12-01T00:55 CET (sv-comp) | ||
94c61e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 36 | 2017-12-02T08:06Z | ||
2d8e1c5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 46 | 2017-12-03T11:13Z |
Found 0 witnesses for program sv-benchmarks/c/systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c, 6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6e1c76d4f66e9e9ebc67a4afc6ce1815d22a2acf5c53a604497fec3c2b5ee232.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |