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/e3775f9d5799542d8458fc045d3139d666c9c33051ec40fda69c260b49493f68.json

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
b9ad233	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2017-12-02T11:48 CET (sv-comp)
b5caa79	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 kind	14	2017-12-01T19:36:14.620477
331a080	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 incr	12	2017-12-01T12:47:10.773508
42bb115	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	75	2017-12-01T19:05 CET (sv-comp)
6cda1ef	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 3.1	75	2017-12-01T04:09 CET (sv-comp)
dedb391	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	125	2017-11-30T11:42:53+01:00
e3775f9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26725	110	2017-11-30T16:47:59+01:00
b9143ae	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CBMC	113	2017-11-30T19:12 CET (sv-comp)
a5a9e77	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	2LS	90	2017-12-01T03:38 CET (sv-comp)
07b7dfe	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T19:44:39.002298
40083a8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0	3	2017-12-02T08:00:16.746401
1adff37	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	CBMC	346	2017-12-01T15:16 CET (sv-comp)
f00c530	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	2LS	739	2017-12-01T12:01 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_spec1_product15_false-unreach-call_true-termination.cil.c, c24f119767bd2b2536e948c8d957853ce547fd14a58f22a874d6d7d99acf9452
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c24f119767bd2b2536e948c8d957853ce547fd14a58f22a874d6d7d99acf9452.json