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/5e67b13ff246ea1bbc5f57fa43cc75a83213ecc2a808b48aad3fbfcc72032ea4.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json

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

Found 11 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
a87f5ea	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Taipan	198	2017-12-03T02:18Z
222e83b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	85	2017-12-03T07:01:15+01:00	c0cd19b
c03d096	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	85	2017-12-03T02:10:29+01:00	a777f0f
7edb71a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	85	2017-12-01T05:23:30+01:00	2bbd026
ceb9361	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	85	2017-12-01T05:22:41+01:00	f2497c5
3acedd7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	85	2017-12-01T04:58:47+01:00	b120fa4
915206f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	85	2017-11-30T12:53:36+01:00
1cd6f0e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	13	2017-12-01T02:09:30+01:00
34bda9f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26725	85	2017-11-30T17:23:37+01:00
55074f7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker (unknown version)	78	2017-12-02T07:07:55+01:00
5e67b13	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Automizer	199	2017-12-02T11:53Z

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i, 573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/573729a2986dc47b40846f118e18b518c7414f31416943d5f9bf9ab16122235c.json