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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Found 0 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json

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

Found 0 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json

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

Found 0 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json

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

Found 0 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json

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

Found 4 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
8dd4b4e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	GACAL	6	2019-12-07T23:15 CET (comp)
13b8b8b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	6	2019-12-08T00:01:20+01:00	8dd4b4e
6f3a277	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	6	2019-11-30T17:39:41+01:00	ec2b4ab
ec2b4ab	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / svcomp20	449	2019-11-30T11:18:39+01:00

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

Found 3 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
565854d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T13:03:21
241e5d7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-09T21:21:16+01:00	76cd767
334b9b4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-08T21:51:57+01:00	565854d

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

Found 3 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
f9fe9cb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	8	2017-11-30T20:24 CET (sv-comp)
3fdaa83	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	6	2017-12-01T08:28:48+01:00	ae20f17
c41000d	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	2LS	11	2017-12-01T14:32 CET (sv-comp)

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

Found 0 witnesses for program sv-benchmarks/c/loop-new/count_by_nondet_true-unreach-call_true-termination.i, 11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/11ed1370ff69738d5f8486a424b5919121bbebf62f2759c85666a40c541ad9c6.json