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

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

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json

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

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json

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

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json

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

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json

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

Found 2 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
2ff3ed3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	33	2019-12-11T21:09:41+01:00	66de1f3
08b9205	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Symbiotic	4	2019-12-01 08:47:57

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

Found 3 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
7a45e31	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	8	2018-12-08T14:15 CET (sv-comp)
cc8216b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	10829	2018-12-08T23:44:04+01:00	7a45e31
572a69e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	33	2018-12-08T04:18:25+01:00	eb79f94

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

Found 2 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
7d109d1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	8	2017-12-01T23:49 CET (sv-comp)
f94a08f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker (unknown version)	31	2017-12-01T20:59:52+01:00

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

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c, 79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/79eedb785fbb159881dc8153d85d0bb7e65a8d2ded64ea39afb48bd591767b54.json