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/43e052896762f4408fca5a36968c2a686286e7c22ad725d8a3cd61f0247b49c5.json

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
a47ec04	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2017-12-02T00:48 CET (sv-comp)
8f74c1b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 kind	4	2017-12-02T02:32:02.640145
34f8815	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 incr	4	2017-12-01T14:36:16.230838
522fb5d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	99	2017-12-01T20:56 CET (sv-comp)
d2a4f86	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	99	2017-12-01T04:27 CET (sv-comp)
4aa4fcf	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	262	2017-11-30T13:42:10+01:00
368561a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	175	2017-12-01T03:26 CET (sv-comp)
43e0528	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	2LS	202	2017-12-01T01:12 CET (sv-comp)
166ca9e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-03T02:08:36.415081
53d1a4a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T10:54:51.700941
f581ee1	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	CBMC	239	2017-12-01T17:18 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_spec3_product28_false-unreach-call_true-termination.cil.c, 9f272f057b38be7a07c72c8df833dbb0667c5f68e1d39e8f73ecc7affb417fd3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9f272f057b38be7a07c72c8df833dbb0667c5f68e1d39e8f73ecc7affb417fd3.json