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/product-lines/email_spec27_product30_false-unreach-call_true-termination.cil.c, ba7e73d48a1cbf115cb84bf02bacedbf5dd0909bf2b907cdc4af94687e083861
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ba7e73d48a1cbf115cb84bf02bacedbf5dd0909bf2b907cdc4af94687e083861.json

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

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

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
abb3bae	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2017-12-02T09:16 CET (sv-comp)
ee9d2b0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 kind	23	2017-12-01T20:15:37.873336
8e3476e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 incr	22	2017-12-01T08:48:44.600954
bc16354	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	112	2017-12-01T16:20 CET (sv-comp)
cc6eee9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	112	2017-12-01T03:16 CET (sv-comp)
94a66f7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	187	2017-12-01T01:05:45+01:00
a2bb033	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26725	162	2017-11-30T16:04:53+01:00
d363c01	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	156	2017-11-30T21:54 CET (sv-comp)
fe99d0b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	2LS	147	2017-11-30T17:57 CET (sv-comp)
ae5630c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-03T00:14:37.634631
1833bb7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T13:37:57.804909
aa66e97	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	CBMC	414	2017-12-01T16:59 CET (sv-comp)
f542c50	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	2LS	986	2017-12-01T12:03 CET (sv-comp)

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

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