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/56457b5c090dd7d09d3987d00ca3f47780c45982c66a8d4f87e5f3f735f7ae2f.json

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

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json

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

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json

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

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json

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

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json

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

Found 6 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
a701b6e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	5	2019-12-01 23:09:12
cf24c31	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	6110	2019-12-11T21:09:30+01:00	a701b6e
7b6eb27	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	6110	2019-12-11T20:55:33+01:00	ed6c45b
7a11496	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	6110	2019-12-11T20:44:41+01:00	75bffd2
6f4c2bd	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / witnessValidation	6110	2019-12-03T08:10:58+01:00	02903bf
02903bf	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.9 / svcomp20	6206	2019-11-30T03:04:00+01:00

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

Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
56962a0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	6156	2018-12-10T20:39:10+01:00	455cd46
b9ddca7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	6110	2018-12-09T18:20:34+01:00	a9434ac
4c21a89	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	6110	2018-12-08T04:58:30+01:00	6b71094
d2496e0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	6110	2018-12-06T09:48:21+01:00	60fe69b
60fe69b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	6157	2018-12-05T22:00:42+01:00

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

Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
4bfa88e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 kind	7	2017-12-01T13:59:57.486049
46db718	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	ESBMC 4.6.0 incr	7	2017-12-01T17:57:30.850067
56457b5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26773	3397	2017-11-30T16:00:47+01:00
ea97672	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26758M	7767	2017-11-30T18:33:24+01:00
e95e1fa	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	2LS	2233	2017-11-30T21:09 CET (sv-comp)

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

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem04_label39_false-unreach-call.c, 48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/48180a2b49a06b2e317170596140cce26d922dce10e583de5a9fa7294714f469.json