Witness Inspection
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).
View and Validate the Witness
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c |
programSHA |
67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c |
witnessName |
results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.Problem05_label26_false-unreach-call.c.files/witness.graphml |
witnessSHA |
f956f77fe835902c13a4a5731705f4fbe3f7cfd74c6894faf92a108e7898b486 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/f956f77fe835902c13a4a5731705f4fbe3f7cfd74c6894faf92a108e7898b486.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-11-30T19:54 CET (sv-comp) |
producer |
2LS |
program-sha256 |
67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c |
programhash |
2462155244f03f72d4fd9bbe9efbda5e841d1807 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/f956f77fe835902c13a4a5731705f4fbe3f7cfd74c6894faf92a108e7898b486.graphml |
witness-sha256 |
f956f77fe835902c13a4a5731705f4fbe3f7cfd74c6894faf92a108e7898b486 |
witness-size |
2394755 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 7 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b691b55 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
6549 |
2019-12-11T21:46:22+01:00 |
0e18e84 |
8618725 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
6548 |
2019-12-11T20:54:35+01:00 |
5cee89a |
a9f1231 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
6548 |
2019-12-11T20:44:52+01:00 |
fa12315 |
fb6c9c3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
6582 |
2019-12-08T01:52:27+01:00 |
62948b1 |
cb497a3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
6549 |
2019-12-03T08:10:29+01:00 |
46102aa |
46102aa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
6651 |
2019-11-30T14:35:32+01:00 |
|
0e18e84 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
6611 |
2019-11-30T23:51:53+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 8 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
43d2278 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
6651 |
2018-12-06T23:57:34+01:00 |
|
1a93031 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6582 |
2018-12-10T20:35:46+01:00 |
f2384bc |
7a16d33 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6548 |
2018-12-09T18:04:00+01:00 |
5a00acb |
e37f135 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6549 |
2018-12-08T09:01:52+01:00 |
43d2278 |
209aece |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6549 |
2018-12-08T05:00:38+01:00 |
7822c5c |
b94327b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6549 |
2018-12-06T10:18:49+01:00 |
68d7299 |
f754c0d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6549 |
2018-12-06T09:48:57+01:00 |
81109d6 |
81109d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6651 |
2018-12-06T06:48:30+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
896b5f5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
5 |
2017-12-02T04:50:12.968958 |
|
2d9c0b5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
5 |
2017-12-01T17:03:00.548858 |
|
61e6b26 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
3647 |
2017-11-30T18:21:12+01:00 |
|
fee6c4b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
2393 |
2017-12-01T02:25 CET (sv-comp) |
|
f956f77 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
2395 |
2017-11-30T19:54 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |