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/30c67d261c8441a26e481a8d4e0cff0e52bcfa94806631d8c49b5a0e3067d906.json

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

Found 0 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json

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

Found 0 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json

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

Found 0 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json

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

Found 0 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json

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

Found 2 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
fdbc7ed	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	11	2019-11-30T16:27:01+01:00	eec3c12
eec3c12	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / svcomp20	11	2019-11-30T06:12:12+01:00

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

Found 4 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
b5d163c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	11	2018-12-08T02:50:54+01:00
d224a92	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-08T06:15:34+01:00	b5d163c
a45a224	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-06T09:24:00+01:00	90b4b4a
90b4b4a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-05T13:38:47+01:00

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

Found 2 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
30c67d2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26725	9	2017-11-30T23:10:11+01:00
451409c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker (unknown version)	10	2017-12-02T05:08:44+01:00

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

Found 0 witnesses for program sv-benchmarks/c/float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c, 1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1f8128f825c5e1c8359e47155215f663439644a7105da75dbb46a99198caac63.json