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)

Key	Value
programName	sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c
programSHA	3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
witnessName	results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.Problem14_label15_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA	b6264a76e0bd1a9b33232f7e9013643ac02667823ad85e570d7489ed9b381cda

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/b6264a76e0bd1a9b33232f7e9013643ac02667823ad85e570d7489ed9b381cda.json

Key	Value
architecture	32bit
creationtime	2017-12-01T16:50 CET (sv-comp)
producer	2LS
program-sha256	3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
programfile	../../sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c
programhash	d7e0aa8bfb25088281b46305e78bdc6c2adff9ac
sourcecodelang	C
specification	CHECK( init(main()), LTL(F end) )
witness-file	witnessFileByHash/b6264a76e0bd1a9b33232f7e9013643ac02667823ad85e570d7489ed9b381cda.graphml
witness-sha256	b6264a76e0bd1a9b33232f7e9013643ac02667823ad85e570d7489ed9b381cda
witness-size	575292
witness-type	violation_witness

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 10 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
24bd4aa	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	301	2019-12-11T20:17:29+01:00	2850c38
b569a18	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	301	2019-12-11T20:07:08+01:00	1f5f4f3
b650278	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	301	2019-12-11T20:02:29+01:00	dc12646
0e0355d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	301	2019-12-08T00:36:39+01:00	a5a9a03
b0d9892	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	301	2019-12-07T19:46:10+01:00	e666aec
12fedee	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	301	2019-12-05T19:03:09+01:00	ee8cc8f
5bb7c1d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	301	2019-11-30T16:23:22+01:00	8d459e4
8d459e4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / svcomp20	303	2019-11-29T16:04:51+01:00
1f5f4f3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco	304	2019-12-01T16:46:31+01:00
7c493e2	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Symbiotic	4	2019-12-02 03:21:58

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 10 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
57ee686	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	309	2018-12-07T16:46:54+01:00
ad831fc	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-10T19:48:53+01:00	c8dd5b3
4e47c80	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-09T20:25:04+01:00	28fcceb
f5160bc	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-09T17:13:49+01:00	ee491ab
4b2c38f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-08T07:10:30+01:00	57ee686
799a58a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-08T03:30:56+01:00	ab7cbf4
7db765e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-06T09:28:26+01:00	e6651dd
963905b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-06T09:07:01+01:00	6e9a7c7
a828014	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	301	2018-12-06T08:03:07+01:00	74c3694
6e9a7c7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	310	2018-12-05T06:21:31+01:00

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 14 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
03f2e4c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Kojak	234	2017-12-02T09:01Z
5e7ff5b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.12-svcomp17	4	2017-11-02T13:16:17+05:30
0d79247	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	301	2017-12-03T04:13:12+01:00	42b393f
dd391a1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	301	2017-12-03T02:46:59+01:00	fb11c60
0bb8bf7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	301	2017-12-03T01:41:35+01:00	9d8e8a5
84f1cd9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	301	2017-12-01T06:50:41+01:00	98a299b
3f5d3b2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	301	2017-12-01T06:15:07+01:00	80259d3
9f8fa60	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	301	2017-12-01T06:11:33+01:00	623f82e
b746f77	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	300	2017-11-30T17:21:07+01:00
5486a42	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26725	300	2017-12-01T01:57:39+01:00
9e94072	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Automizer	210	2017-12-02T06:51Z
a0c47be	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	2LS	997	2017-11-30T11:41 CET (sv-comp)
e08736e	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Automizer	147	2017-12-03T11:13Z
b6264a7	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	2LS	575	2017-12-01T16:50 CET (sv-comp)

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

Trying to find witnesses for program (3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d, sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c, 3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3bb2090f690b42b42edaa49a49c191b3cc174d4f50f33dfa1d1bb22670545d1d.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness