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/f773b8e52cad099161cd3d78a6d17704003db99a8be846524b84c5953cad8e5a.json

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

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

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

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

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

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

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

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

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

Found 6 witnesses for program sv-benchmarks/c/product-lines/elevator_spec13_product31_true-unreach-call_false-termination.cil.c, 309a3d2bdd84f1ccb7d9ed71ec53debcf527e709ae70f42a24c2be64f7b156c5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/309a3d2bdd84f1ccb7d9ed71ec53debcf527e709ae70f42a24c2be64f7b156c5.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
1667a22	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	327	2019-12-11T20:08:16+01:00	0adefb9
4ef91f0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	327	2019-11-30T19:23:41+01:00	f7d6b36
7a8b985	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	327	2019-11-30T16:40:14+01:00	df1dbad
df1dbad	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / svcomp20	327	2019-11-30T04:04:22+01:00
0adefb9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco	327	2019-12-01T09:03:20+01:00
a6e9e5e	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Symbiotic	1	2019-12-02 04:19:48

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

Found 9 witnesses for program sv-benchmarks/c/product-lines/elevator_spec13_product31_true-unreach-call_false-termination.cil.c, 309a3d2bdd84f1ccb7d9ed71ec53debcf527e709ae70f42a24c2be64f7b156c5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/309a3d2bdd84f1ccb7d9ed71ec53debcf527e709ae70f42a24c2be64f7b156c5.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
20ccfd7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T09:50:12
313c42e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	327	2018-12-07T00:40:57+01:00
6b694e9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	327	2018-12-10T10:45:53+01:00	18348fd
0d948c2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	327	2018-12-08T21:54:37+01:00	20ccfd7
eb42f64	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	327	2018-12-08T06:22:01+01:00	313c42e
9dc6564	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	327	2018-12-08T02:12:33+01:00	18348fd
b845a62	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	327	2018-12-06T09:43:06+01:00	f773b8e
8b04ce3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	327	2018-12-06T09:26:51+01:00	75eeeab
75eeeab	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	327	2018-12-05T21:03:47+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_product31_true-unreach-call_false-termination.cil.c, 309a3d2bdd84f1ccb7d9ed71ec53debcf527e709ae70f42a24c2be64f7b156c5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/309a3d2bdd84f1ccb7d9ed71ec53debcf527e709ae70f42a24c2be64f7b156c5.json

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

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