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)

Key	Value
programName	sv-benchmarks/c/product-lines/elevator_spec9_product25_true-unreach-call_true-termination.cil.c
programSHA	bd6734a33372dc6f2f681c8b5001a225244cc9fc5e77ce4f6e9ad1a038fd2768
witnessName	results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.elevator_spec9_product25_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA	23a5d7532348d5d37e41462faccf1f86b76a0187381a1d97d3a05d603f67de61

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/23a5d7532348d5d37e41462faccf1f86b76a0187381a1d97d3a05d603f67de61.json

Key	Value
architecture	32bit
creationtime	2017-12-01T00:13:09+01:00
producer	CPAchecker 1.6.1-svn
program-sha256	bd6734a33372dc6f2f681c8b5001a225244cc9fc5e77ce4f6e9ad1a038fd2768
programfile	/tmp/vcloud-vcloud-master/worker/working_dir_6efc3497-a28c-4ad6-98ac-a43d8d96ed81/sv-benchmarks/c/product-lines/elevator_spec9_product25_true-unreach-call_true-termination.cil.c
programhash	9615097caec3361f31cef4b47d1cac6f6843f6d3
sourcecodelang	C
specification	CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file	witnessFileByHash/23a5d7532348d5d37e41462faccf1f86b76a0187381a1d97d3a05d603f67de61.graphml
witness-sha256	23a5d7532348d5d37e41462faccf1f86b76a0187381a1d97d3a05d603f67de61
witness-size	3961
witness-type	correctness_witness

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
9b1bd3d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2017-12-02T00:12 CET (sv-comp)
a6ef428	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T22:08:14.426752
eac9672	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T15:24:27.770431
8c37e3d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 kind	3	2017-12-02T00:08:51.444868
476b328	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 incr	3	2017-12-01T11:07:22.600775
c47ba29	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	69	2017-12-01T20:58 CET (sv-comp)
ea2422a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn	296	2017-12-03T03:01:20+01:00
23a5d75	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn	4	2017-12-01T00:13:09+01:00
8c513f0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	296	2017-12-03T04:21:05+01:00	f38aa05
fb926f0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	296	2017-12-02T20:39:47+01:00	362bf68
1d68cba	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	296	2017-12-02T07:50:58+01:00	8b774fd
f4e2727	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	296	2017-12-01T22:25:33+01:00	349d702
abacdee	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	296	2017-12-01T08:14:24+01:00	def76d3
1b3ca56	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	296	2017-12-01T06:28:06+01:00	da9689f
1792f29	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	296	2017-12-01T06:11:29+01:00	bb70295
f419879	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	297	2017-11-30T21:09:37+01:00
6be300b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CBMC	210	2017-11-30T18:20 CET (sv-comp)
706d638	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	2LS	11033	2017-11-30T15:12 CET (sv-comp)
8d07936	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	CBMC	210	2017-12-01T14:12 CET (sv-comp)
1ca68e6	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	2LS	3625	2017-12-01T16:11 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_spec9_product25_true-unreach-call_true-termination.cil.c, bd6734a33372dc6f2f681c8b5001a225244cc9fc5e77ce4f6e9ad1a038fd2768
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bd6734a33372dc6f2f681c8b5001a225244cc9fc5e77ce4f6e9ad1a038fd2768.json

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