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

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

Found 0 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json

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

Found 0 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json

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

Found 0 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json

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

Found 0 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json

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

Found 0 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json

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

Found 0 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json

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

Found 7 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
dd03af5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26725	2	2017-11-30T13:26:58+01:00
5efeb3b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	54	2017-12-02T14:51:43+01:00	6feb940
579d5b7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	54	2017-12-01T06:02:27+01:00	253db02
bb99f39	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	54	2017-12-01T04:56:26+01:00	2dd559c
66af34f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	55	2017-11-30T15:32:06+01:00
a58a9a0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	37	2017-12-01T02:12:10+01:00
b687ad1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker (unknown version)	49	2017-12-02T01:55:39+01:00

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

Found 0 witnesses for program sv-benchmarks/c/ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c, aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/aa2814b52985befb278863f3e1cfeb77a5d113feabb5c23f51c75d892e381c38.json