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/2019/results/witnessInfoByHash/6f1d9a0261066104d4c55f6719afa69114ea40a289a3edb57d247aa1493a3daf.json

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

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

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

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

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

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

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

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

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

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

Found 7 witnesses for program sv-benchmarks/c/product-lines/elevator_spec13_product30_true-unreach-call_false-termination.cil.c, 21a5887fd1c368fd8903912da8c6932fa641cecb8b6029f7382d0bacdeba1c3b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/21a5887fd1c368fd8903912da8c6932fa641cecb8b6029f7382d0bacdeba1c3b.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
37e2083	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	323	2019-12-11T20:15:28+01:00	562fc39
585bf0d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	323	2019-12-11T20:02:26+01:00	327f380
ad91d5e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	323	2019-11-30T19:41:01+01:00	d9741fc
0e9c519	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	323	2019-11-30T17:17:05+01:00	ab5e508
ab5e508	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / svcomp20	323	2019-11-30T12:03:03+01:00
562fc39	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco	323	2019-12-01T01:40:56+01:00
354fe8e	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Symbiotic	1	2019-12-01 07:42:08

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

Found 8 witnesses for program sv-benchmarks/c/product-lines/elevator_spec13_product30_true-unreach-call_false-termination.cil.c, 21a5887fd1c368fd8903912da8c6932fa641cecb8b6029f7382d0bacdeba1c3b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/21a5887fd1c368fd8903912da8c6932fa641cecb8b6029f7382d0bacdeba1c3b.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
c4d0001	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T09:36:32
40aea23	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	323	2018-12-10T10:45:27+01:00	0677ede
b4683a4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	323	2018-12-08T21:55:00+01:00	c4d0001
6f1d9a0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	323	2018-12-08T02:56:40+01:00	3763218
37adb64	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	323	2018-12-08T02:37:17+01:00	0677ede
544a9d9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	323	2018-12-06T09:43:45+01:00	3d28704
68b82b9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	323	2018-12-06T09:00:12+01:00	89dea4f
89dea4f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	323	2018-12-05T19:49:45+01:00

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

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec13_product30_true-unreach-call_false-termination.cil.c, 21a5887fd1c368fd8903912da8c6932fa641cecb8b6029f7382d0bacdeba1c3b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/21a5887fd1c368fd8903912da8c6932fa641cecb8b6029f7382d0bacdeba1c3b.json

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

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