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/floats-esbmc-regression/fmod2_true-unreach-call.i
programSHA	c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
witnessName	results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.fmod2_true-unreach-call.i.files/witness.graphml
witnessSHA	ad64b02fe291d077419ad217d5a27458cb36e37f0ee1bc138462cf610d25ff68

Information about the Witness from Competition Database

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

Key	Value
architecture	32bit
creationtime	2017-12-02T19:27:01+01:00
producer	CPAchecker 1.6.1-svn
program-sha256	c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
programfile	/home/benchexec/ar_abs_temp/fmod2_true_unreach_call.c
programhash	3f33e4997286b8a1220e37dd20242853da524fd9
sourcecodelang	C
specification	CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file	witnessFileByHash/ad64b02fe291d077419ad217d5a27458cb36e37f0ee1bc138462cf610d25ff68.graphml
witness-sha256	ad64b02fe291d077419ad217d5a27458cb36e37f0ee1bc138462cf610d25ff68
witness-size	8034
witness-type	correctness_witness

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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 14 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
4475feb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Pinaka	3	2019-12-04T00:41 CET (comp)
1e6728d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-11T20:15:23+01:00	40d92cd
e25e2dc	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-11T20:07:18+01:00	0ddf095
3e9212d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-11T20:02:17+01:00	91a9e9f
7bc73ed	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-08T00:37:12+01:00	a31084b
a843710	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-07T23:45:35+01:00	c7df484
6f0c695	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-05T19:13:31+01:00	a029512
dd1201b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-05T19:03:04+01:00	35213ec
d378ca5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-04T02:07:52+01:00	4475feb
963e50f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-11-30T16:50:16+01:00	1984ad2
1984ad2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / svcomp20	7	2019-11-30T08:03:09+01:00
a31084b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.8	6	2019-12-07T22:21:28+01:00
0ddf095	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco	7	2019-12-01T00:17:10+01:00
c7df484	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	BRICK	3	2019-12-07T21:41:43Z

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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 13 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
1441ff6	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Pinaka	3	2018-12-07T05:26 CET (sv-comp)
772fa2a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7	7	2018-12-10T19:17:02+01:00
7230c48	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	7	2018-12-07T10:52:20+01:00
cb8c8a4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-10T19:49:28+01:00	772fa2a
4a30d53	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-08T05:43:43+01:00	7230c48
9ad9cc0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-08T02:54:59+01:00	5e476df
59d9b37	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-07T17:45:58+01:00	a1f7fb0
2621d51	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-07T16:25:49+01:00	1441ff6
a193fc1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-06T09:28:46+01:00	a9c5e98
e107b42	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-06T08:56:28+01:00	2fa719c
eebf741	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-06T08:17:01+01:00	d313c48
8f80d49	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-06T07:51:40+01:00	8c4251a
2fa719c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-05T09:31:20+01:00

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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
b259c7f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn	7	2017-11-30T20:41:36+01:00
bd11f43	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26758M	16	2017-12-01T01:23:46+01:00
bb95c39	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26725	6	2017-11-30T12:04:48+01:00
d77c8df	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker (unknown version)	7	2017-12-02T09:12:58+01:00
3568eec	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 kind	3	2017-12-01T19:54:39.650760
c45715d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 incr	3	2017-12-01T08:09:59.354956
ad64b02	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn	8	2017-12-02T19:27:01+01:00
7f6ac1a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	8	2017-12-03T03:59:08+01:00	97c820a
118b70c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	8	2017-12-02T08:38:09+01:00	64933dc
622e8f8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	8	2017-12-01T22:22:47+01:00	fe20a52
7bed634	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	8	2017-12-01T07:12:43+01:00	8893eb5
befe560	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	8	2017-12-01T05:46:10+01:00	f8a19fe
746c1e3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	8	2017-12-01T05:39:11+01:00	9d87a09
ffdf0e2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	8	2017-11-30T20:43:30+01:00
2b9e3bc	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CBMC	9	2017-11-30T16:34 CET (sv-comp)
a9526fb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	2LS	68	2017-11-30T16:53 CET (sv-comp)

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

Trying to find witnesses for program (c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057, sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/fmod2_true-unreach-call.i, c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c20e63da09cc334b4b6164d7f98459eee7c0451de598c739d6be443c17809057.json

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