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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.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 (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.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 (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.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 (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.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 (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.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 '19

Trying to find witnesses for program (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 24 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6474ea8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2018-12-08T03:15 CET (sv-comp)
Download de7f603 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T10:00:53
Download 28a85bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 7 2018-12-07T15:07 CET (sv-comp)
Download dbdcf71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 11 2018-12-10T18:10:29+01:00
Download 3d0bdbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 12 2018-12-06T20:05:00+01:00
Download 364912b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-10T20:36:58+01:00 Download dbdcf71
Download 81a33b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-09T21:23:32+01:00 Download ed8b73a
Download 19e222e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-09T20:53:05+01:00 Download 454b565
Download 3db8088 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-09T20:36:46+01:00 Download 824d093
Download 22852f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-09T20:35:11+01:00 Download 792ebce
Download 354410d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T18:16:42+01:00 Download efde9d7
Download 6f882fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T23:44:07+01:00 Download 6474ea8
Download f16d100 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T22:07:25+01:00 Download de7f603
Download ba0e997 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T05:03:20+01:00 Download fcd748d
Download dd4ae23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-07T18:47:41+01:00 Download 0f007b7
Download 1c399af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:44:49+01:00 Download 28a85bc
Download 673f1f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-06T10:19:44+01:00 Download 1a4c013
Download 3960f2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-06T09:47:54+01:00 Download 6acb9ac
Download 2295624 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:12:00+01:00 Download 2031971
Download 6acb9ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-05T20:48:08+01:00
Download b770821 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T09:04:18+01:00 Download 3d0bdbc
Download 5b406eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-07T01:20:42+01:00 Download 2ac0ceb
Download 943d187 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:42:00+01:00 Download b5a5054
Download f22c899 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:07:05+01:00 Download d033e18

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

Trying to find witnesses for program (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 20 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 01acc01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 4 2017-12-01T23:41 CET (sv-comp)
Download 1a4131b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 8 2017-12-03T04:00 CET (sv-comp)
Download 1359691 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 10 2017-12-03T04:43Z
Download f9bc3ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T06:55 CET (sv-comp)
Download c3b6a9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 9 2017-12-02T17:34Z
Download e47d1b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T18:39:42.497478
Download 1c906f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T07:50:00.074341
Download 2ac8dfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-12-01T18:46 CET (sv-comp)
Download f53e405 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-11-30T21:50 CET (sv-comp)
Download aca2ead Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 11 2017-12-03T01:36:14+01:00
Download 0105c7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 11 2017-11-30T19:13:52+01:00
Download 1e79504 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 14 2017-11-30T20:46:57+01:00
Download 91c1875 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 8 2017-11-30T15:23:34+01:00
Download 6087e75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 10 2017-12-02T10:47:23+01:00
Download d49f940 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 8 2017-11-30T21:12 CET (sv-comp)
Download b7d014c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 10 2017-12-02T12:26Z
Download 2a28e4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 8 2017-11-30T21:27 CET (sv-comp)
Download 588f6a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T20:59 CET (sv-comp)
Download d72bc78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T22:37:23+01:00 728b28d
Download 79d4261 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 17 2017-12-01T14:43 CET (sv-comp)

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

Trying to find witnesses for program (a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16, sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i, a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a83182ff622fde821e298074dbcd99805d50d2f59350b297b9709629661bce16.json

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