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/40a3b98142330d8b93798de662b7311f798ff9730cb8e26cc99ee7adac85348f.json

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

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json

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

Found 1 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
14b9590	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Bubaak	3	2022-12-08T14:19:44Z

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

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json

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

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json

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

Found 2 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
e0dc03d	Inspect		CHECK( init(main()), LTL(G valid-free) )	correctness_witness	CPAchecker 1.9	6	2019-11-29T19:17:09+01:00
bb26e71	Inspect		CHECK( init(main()), LTL(G valid-free) )	correctness_witness	CPAchecker 1.8-svn-35b8bb3bb3+	6	2019-12-01T08:10:58+01:00

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

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json

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

Found 1 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
40a3b98	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	6	2017-12-01T21:16 CET (sv-comp)

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

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/2Nested_true-termination_true-valid-memsafety.c, 98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/98e3578cd96fe8b8eee528450509f182c2f5e45fbe2813a1c7e5d95c43606358.json