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/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c |
programSHA |
beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a |
witnessName |
results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.email_spec1_product22_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA |
35b1f03bde303766559853b0128a90c5b9b659792a4307893c4a56a7d0cad0fa |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/35b1f03bde303766559853b0128a90c5b9b659792a4307893c4a56a7d0cad0fa.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T03:06 CET (sv-comp) |
producer |
CBMC |
program-sha256 |
beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a |
programfile |
../../sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c |
programhash |
6a57a7b4ef4bd4310a90335fc13bc2a1fff918f6 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/35b1f03bde303766559853b0128a90c5b9b659792a4307893c4a56a7d0cad0fa.graphml |
witness-sha256 |
35b1f03bde303766559853b0128a90c5b9b659792a4307893c4a56a7d0cad0fa |
witness-size |
91858 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.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 (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.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 (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.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 (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.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 (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.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 '19
Trying to find witnesses for program (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.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 '18
Trying to find witnesses for program (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 12 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
152680a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T06:48 CET (sv-comp) |
|
7e817a5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
14 |
2017-12-01T19:38:34.807031 |
|
dc98ed1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
14 |
2017-12-01T16:05:49.651946 |
|
05efae9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
77 |
2017-12-01T18:24 CET (sv-comp) |
|
33d8e5b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
76 |
2017-12-01T00:36 CET (sv-comp) |
|
ff6f80d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
128 |
2017-11-30T12:30:39+01:00 |
|
35b1f03 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
92 |
2017-12-01T03:06 CET (sv-comp) |
|
ffba8a2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
113 |
2017-11-30T19:21 CET (sv-comp) |
|
7e64218 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T23:08:04.190476 |
|
e615c4d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T15:24:04.993611 |
|
bf0e7e0 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
398 |
2017-12-01T14:42 CET (sv-comp) |
|
d1bc25b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
918 |
2017-12-01T15:16 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a, sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c, beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/beb933c7449a14a8c8614d68c3082a760d297a13b193009e267a11d4b3c2212a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |