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

• View Witness
• 
  Click on the button to verify this program using this witness, and inpect the validation results, e.g., explore the ARG or error path.

Input Given to this Service about the Witness (URL Query)

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/1f175e34144fb28c5a0d12bc00c51267c9e01f952382bf43c7b3248cc6fa354d.json

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

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

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

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

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

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

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

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

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

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

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

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

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

Found 12 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product32_false-unreach-call_true-termination.cil.c, bf6df77f2853229d41f9f3a928787c8c30433396696562c9d23097dea2dd2e19
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bf6df77f2853229d41f9f3a928787c8c30433396696562c9d23097dea2dd2e19.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
b8d6f07	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2017-12-02T17:34 CET (sv-comp)
2592fe9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 kind	4	2017-12-01T14:02:27.000360
06e44b7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 incr	4	2017-12-01T14:30:36.214269
bd9fe43	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	70	2017-12-01T15:57 CET (sv-comp)
2f9439d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	70	2017-12-01T06:39 CET (sv-comp)
1f175e3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	190	2017-11-30T12:36:06+01:00
f6b7065	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	122	2017-11-30T13:13 CET (sv-comp)
b9eadcb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	2LS	141	2017-11-30T21:49 CET (sv-comp)
957eb29	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T21:11:15.600500
7db38ed	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T11:58:32.887660
b8918d4	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	CBMC	112	2017-12-01T19:08 CET (sv-comp)
7a39306	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	2LS	12213	2017-12-01T14:08 CET (sv-comp)

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

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