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/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c
programSHA	9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6
witnessName	results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.email_spec27_product18_false-unreach-call_true-termination.cil.c.files/witness.graphml
witnessSHA	ce1577ecc09fddda5ed5ac2523d714c60f53f3c290dbe681e8e539f8dd6de2b8

Information about the Witness from Competition Database

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

Key	Value
architecture	32bit
creationtime	2017-12-02T00:32 CET (sv-comp)
producer	Symbiotic
program-sha256	9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6
programfile	/tmp/vcloud-vcloud-master/worker/working_dir_1fe7f43f-f448-4224-a396-bf52483f8d4c/sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c
programhash	551ff497dc22db89344937444016f53dc662cf3d
sourcecodelang	C
specification	CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file	witnessFileByHash/ce1577ecc09fddda5ed5ac2523d714c60f53f3c290dbe681e8e539f8dd6de2b8.graphml
witness-sha256	ce1577ecc09fddda5ed5ac2523d714c60f53f3c290dbe681e8e539f8dd6de2b8
witness-size	816
witness-type	violation_witness

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

Trying to find witnesses for program (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c, 9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6.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 (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c, 9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6.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 (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c, 9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6.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 (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c, 9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6.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 (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
f682284	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	2	2019-12-01 18:53:08
c44fe10	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	172	2019-12-11T21:40:19+01:00	89bcf14
cccdcd7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	184	2019-12-11T21:09:48+01:00	f682284
311c40a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	172	2019-12-11T20:54:56+01:00	aeb07f0
0e1cf8c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	190	2019-12-11T20:44:28+01:00	dda8e92
c30dc31	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	173	2019-12-08T01:51:50+01:00	a0e8c11
7916529	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	215	2019-12-03T08:56:57+01:00	9bae2eb
9572c53	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	172	2019-12-03T08:06:11+01:00	30dfb32
30dfb32	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / svcomp20	159	2019-11-30T12:44:02+01:00
a0e8c11	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.8	176	2019-12-07T22:05:35+01:00
89bcf14	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco	173	2019-12-01T11:10:13+01:00
015210e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	152	2019-12-05T20:21:41+01:00	1923320
f4586a9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	152	2019-12-05T19:34:07+01:00	9ed280e

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

Trying to find witnesses for program (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
a7e9d6f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2018-12-08T11:52 CET (sv-comp)
6e3a2ff	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	28	2018-12-08T06:09:57
41459b0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Pinaka	125	2018-12-07T10:27 CET (sv-comp)
8361ce4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7	166	2018-12-10T19:10:49+01:00
14b95e8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	174	2018-12-07T15:54:41+01:00
b1b8004	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	173	2018-12-10T20:37:48+01:00	8361ce4
c123a7b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	179	2018-12-09T18:21:57+01:00	47e85f7
1239bd7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	216	2018-12-08T23:43:02+01:00	a7e9d6f
4b815d9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	110	2018-12-08T22:11:13+01:00	6e3a2ff
c0625d2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	172	2018-12-08T08:08:44+01:00	14b95e8
5c3ceee	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	172	2018-12-08T04:56:42+01:00	4e5ce69
d72a642	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	184	2018-12-07T17:44:16+01:00	41459b0
09bc074	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	172	2018-12-06T10:20:00+01:00	5a8dc65
37dd48b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	172	2018-12-06T09:48:59+01:00	305f569
305f569	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	159	2018-12-05T21:43:50+01:00
b328bea	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	152	2018-12-06T09:42:32+01:00	c2230ae
4214484	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	151	2018-12-06T09:08:34+01:00	bbd0a21
c78d881	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Symbiotic	1	2018-12-08T08:19 CET (sv-comp)

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

Trying to find witnesses for program (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
ce1577e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2017-12-02T00:32 CET (sv-comp)
780cdb4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 kind	17	2017-12-01T12:55:39.590077
d8ece47	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 incr	16	2017-12-01T17:43:28.977251
2365edb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	92	2017-12-01T19:28 CET (sv-comp)
fbb6fa3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	92	2017-11-30T20:02 CET (sv-comp)
b827640	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	149	2017-11-30T16:17:01+01:00
5beed63	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26725	134	2017-11-30T20:03:58+01:00
501a3b2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	125	2017-11-30T15:16 CET (sv-comp)
d2e125e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	2LS	115	2017-11-30T11:37 CET (sv-comp)
a80fc89	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-03T00:49:56.717179
90e3b31	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T14:11:38.976436
032e4ee	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	CBMC	359	2017-12-01T14:04 CET (sv-comp)
9738efd	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	2LS	798	2017-12-01T16:56 CET (sv-comp)

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

Trying to find witnesses for program (9e5c75e477dd9a860f332762117c4125e6a58b276d25b874c3ff78809c0c32d6, sv-benchmarks/c/product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c).

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

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