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_spec0_product16_false-unreach-call_true-termination.cil.c
programSHA d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
witnessName results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-reachsafety.email_spec0_product16_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA 7ff9954fcf791c173fd0e7a6c9c0753154ff569e480f33e4fdb1bf76db1221bc

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/7ff9954fcf791c173fd0e7a6c9c0753154ff569e480f33e4fdb1bf76db1221bc.json

Key Value
architecture 32bit
creationtime 2018-12-08T17:26 CET (sv-comp)
producer Symbiotic
program-sha256 d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
programfile /tmp/vcloud-vcloud-master/worker/working_dir_807b9af5-a62d-4b12-91e4-27ce7c36468d/sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c
programhash d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/7ff9954fcf791c173fd0e7a6c9c0753154ff569e480f33e4fdb1bf76db1221bc.graphml
witness-sha256 7ff9954fcf791c173fd0e7a6c9c0753154ff569e480f33e4fdb1bf76db1221bc
witness-size 839
witness-type violation_witness

This witness was created for this program (cf. table above, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d).

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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 (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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 (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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 (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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 (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 13 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c2200e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 11:41:31
Download 82576ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 132 2019-12-11T22:00:45+01:00 Download 825ec1b
Download 7117fa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 105 2019-12-11T21:09:41+01:00 Download c2200e0
Download 902b7d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 105 2019-12-11T20:54:51+01:00 Download ae83d86
Download 6fabd48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 105 2019-12-11T20:44:38+01:00 Download faf67cb
Download a434df9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 117 2019-12-08T01:51:25+01:00 Download 7919587
Download 35356a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 121 2019-12-03T08:56:52+01:00 Download b8bbdc6
Download c3f3a37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 119 2019-12-03T08:08:50+01:00 Download 2253472
Download 2253472 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 111 2019-11-30T04:57:57+01:00
Download 7919587 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 119 2019-12-07T13:00:24+01:00
Download 825ec1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 132 2019-12-01T00:25:56+01:00
Download 8fee31f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 148 2019-12-05T20:21:43+01:00 Download f4c9d8c
Download e55cf91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 148 2019-12-05T19:34:10+01:00 Download a6ad87e

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 18 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7ff9954 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T17:26 CET (sv-comp)
Download a86fa45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 20 2018-12-08T09:22:05
Download cba9f3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 75 2018-12-07T09:00 CET (sv-comp)
Download 1e82c2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 112 2018-12-10T18:08:14+01:00
Download 3c048aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 133 2018-12-07T23:07:27+01:00
Download cef6265 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 117 2018-12-10T20:37:03+01:00 Download 1e82c2e
Download 0f906aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 106 2018-12-09T18:21:57+01:00 Download e8fea8e
Download 8e91d10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 121 2018-12-08T23:43:43+01:00 Download 7ff9954
Download ec22856 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 79 2018-12-08T22:07:27+01:00 Download a86fa45
Download 4ea8bad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 133 2018-12-08T08:34:55+01:00 Download 3c048aa
Download 0251223 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 119 2018-12-08T05:03:26+01:00 Download 4b58f66
Download 1718932 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 105 2018-12-07T17:45:10+01:00 Download cba9f3c
Download 34060ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 131 2018-12-06T10:18:21+01:00 Download 57c916f
Download 69c4cfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 119 2018-12-06T09:48:11+01:00 Download 8adb933
Download 8adb933 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 111 2018-12-05T10:34:18+01:00
Download fefa193 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 148 2018-12-06T09:42:25+01:00 Download f14da1e
Download 0368eaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 148 2018-12-06T09:19:03+01:00 Download 91c9a91
Download 4ac1c8a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T03:23 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.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 '17

Trying to find witnesses for program (d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d, sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c, d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d76a41ceb36d1c62e7aa108a59b1177aa15b100cf21cdcc8760aecd28425289d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness