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/2f326f93f5b8243216857679e75160bcb3ab30942abd497babc6c06d29e3aaff.json

This witness was created for this program (cf. table above, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce).

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

Found 0 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json

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

Found 0 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json

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

Found 0 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json

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

Found 0 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json

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

Found 4 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
c94f958	Inspect		CHECK( init(main()), LTL(G ! overflow) )	correctness_witness	CPAchecker 1.9	21	2019-11-29T15:44:25+01:00
2d7283a	Inspect		CHECK( init(main()), LTL(G ! overflow) )	correctness_witness	CPAchecker 1.8-svn-35b8bb3bb3+	21	2019-12-01T03:54:26+01:00
524c2a0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	20	2019-12-11T20:02:18+01:00	ae333d1
9d9cb43	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	20	2019-12-07T23:30:03+01:00	441e837

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

Found 6 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
88a4223	Inspect		CHECK( init(main()), LTL(G ! overflow) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T01:29:54
f1da184	Inspect		CHECK( init(main()), LTL(G ! overflow) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	21	2018-12-07T00:05:54+01:00
7a7713c	Inspect		CHECK( init(main()), LTL(G ! overflow) )	correctness_witness	CPAchecker 1.7-svn 29852	21	2018-12-06T00:34:49+01:00
83f5971	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T07:33:12
c55da17	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	20	2018-12-08T21:31:36+01:00	83f5971
2f326f9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	20	2018-12-06T09:28:18+01:00	c190204

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

Found 8 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
f034774	Inspect		CHECK( init(main()), LTL(G ! overflow) )	correctness_witness	ESBMC 3.1	39	2017-12-01T14:05 CET (sv-comp)
966aa6d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26758M	27	2017-11-30T22:28:47+01:00
2d8c188	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.6.1-svn 26725	13	2017-12-01T02:59:41+01:00
42e08ca	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker (unknown version)	15	2017-12-02T12:22:11+01:00
ca6d7c0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	39	2017-12-01T16:21 CET (sv-comp)
93de1f8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	39	2017-12-01T05:56 CET (sv-comp)
fba3b04	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	20	2017-12-01T08:13:35+01:00	2441be5
f28f764	Inspect		CHECK( init(main()), LTL(F end) )	violation_witness	Automizer	16	2017-12-03T11:19Z

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

Found 0 witnesses for program sv-benchmarks/c/recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c, 915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/915422def0fb98296e38957999768ad63c058f53ac3d101cda0496119313cdce.json