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_spec1_product11_true-unreach-call_true-termination.cil.c
programSHA	d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
witnessName	results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.elevator_spec1_product11_true-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA	48352415064174ff999f7704988ba8ad11f8312842fde8ea0162584a01437eb8

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/48352415064174ff999f7704988ba8ad11f8312842fde8ea0162584a01437eb8.json

Key	Value
architecture	32bit
creationtime	2017-12-01T02:56 CET (sv-comp)
producer	2LS
program-sha256	d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
programfile	../../sv-benchmarks/c/product-lines/elevator_spec1_product11_true-unreach-call_true-termination.cil.c
programhash	3a4c8bf043c4419fda457fc2133052e3258c5bde
sourcecodelang	C
specification	CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file	witnessFileByHash/48352415064174ff999f7704988ba8ad11f8312842fde8ea0162584a01437eb8.graphml
witness-sha256	48352415064174ff999f7704988ba8ad11f8312842fde8ea0162584a01437eb8
witness-size	17279800
witness-type	correctness_witness

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

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

Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.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_spec1_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.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_spec1_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.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_spec1_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.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_spec1_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.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_spec1_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.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_spec1_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
f2feda9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2017-12-01T23:23 CET (sv-comp)
2950147	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T22:26:36.460958
f748a24	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T15:33:55.934836
5e10844	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 kind	3	2017-12-01T12:40:59.745352
c46061e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 incr	3	2017-12-01T17:56:51.442267
e47dccb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	126	2017-12-01T18:53 CET (sv-comp)
ea259c3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.12-svcomp17	4	2017-11-02T13:16:17+05:30
475d30f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn	4	2017-12-01T07:37:10+01:00
05c3f1d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-03T04:20:03+01:00	4eb574a
d734494	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-02T20:13:50+01:00	2065aaa
a61b71d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-02T08:31:52+01:00	07715cf
89bea56	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-01T22:34:57+01:00	d159d09
5dc1b34	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-01T08:14:37+01:00	f3e42e0
1993bd9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-01T06:46:35+01:00	c0a4326
1d2c00a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-01T05:21:19+01:00	c4fbc2b
df5e0d9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-12-01T02:15:09+01:00
d716997	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CBMC	371	2017-11-30T19:08 CET (sv-comp)
4835241	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	2LS	17280	2017-12-01T02:56 CET (sv-comp)
5193dec	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	CBMC	371	2017-12-01T16:44 CET (sv-comp)
f3e394b	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	2LS	3440	2017-12-01T13:52 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_product11_true-unreach-call_true-termination.cil.c, d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d94a986e0a35e88f6490ffeb643e7004878faeda7bb3f80d30fe12a271a86c18.json

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