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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.email_spec1_product22_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 7e817a5f1c565322196234cbb3f67d9f9b1041b2553f24529c9ee6b34af85e99

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/7e817a5f1c565322196234cbb3f67d9f9b1041b2553f24529c9ee6b34af85e99.json

Key Value
architecture 32bit
creationtime 2017-12-01T19:38:34.807031
producer ESBMC 4.6.0 kind
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/7e817a5f1c565322196234cbb3f67d9f9b1041b2553f24529c9ee6b34af85e99.graphml
witness-sha256 7e817a5f1c565322196234cbb3f67d9f9b1041b2553f24529c9ee6b34af85e99
witness-size 14115
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
Download 152680a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T06:48 CET (sv-comp)
Download 7e817a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 14 2017-12-01T19:38:34.807031
Download dc98ed1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 14 2017-12-01T16:05:49.651946
Download 05efae9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 77 2017-12-01T18:24 CET (sv-comp)
Download 33d8e5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 76 2017-12-01T00:36 CET (sv-comp)
Download ff6f80d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 128 2017-11-30T12:30:39+01:00
Download 35b1f03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 92 2017-12-01T03:06 CET (sv-comp)
Download ffba8a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 113 2017-11-30T19:21 CET (sv-comp)
Download 7e64218 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:08:04.190476
Download e615c4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:24:04.993611
Download bf0e7e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 398 2017-12-01T14:42 CET (sv-comp)
Download d1bc25b Inspect Inspect
Validate
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