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/2019/results/witnessInfoByHash/bfba204ce907ac6d986ceb9e1668a89db7b753312ae52ae3469a4620982073ff.json

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

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json

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

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json

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

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json

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

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json

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

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json

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

Found 8 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
652d18c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	12	2018-12-08T03:52:49
7b39f74	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	28	2018-12-06T20:13:36+01:00
8f22f07	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	33	2018-12-08T22:10:28+01:00	652d18c
a7074b7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	31	2018-12-08T09:00:15+01:00	7b39f74
0879834	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	30	2018-12-06T09:49:21+01:00	7dd3848
7dd3848	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	27	2018-12-05T23:54:06+01:00
2f61200	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	595	2018-12-06T09:15:25+01:00	2848881
ec79dcc	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	595	2018-12-06T09:11:32+01:00	51473e9

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

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json

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

Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_false-unreach-call.i.cil.c, ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ff61bdda9db90616e1b0532cb72720a413902d3801978a94db2cbc720a4cba6c.json