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 (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.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 (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.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 (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.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 (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.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 (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 17 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e772b51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-11-29T23:46:45+01:00
Download f8a9c96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T01:54:43+01:00
Download 0c94c3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 07:08:30
Download 1f576bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T22:00:33+01:00 Download 5dde02c
Download f0db04b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T22:00:06+01:00 Download e8cb7b7
Download 496477b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T21:09:41+01:00 Download 0c94c3f
Download 96ac0aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:44:34+01:00 Download fb5a95c
Download 70b4fa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-08T00:26:05+01:00 Download 9de0c57
Download e723ea1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T21:17:38+01:00 Download e6fd69a
Download f6b18d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T20:20:13+01:00 Download 2cb2078
Download 2d447d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-03T08:56:54+01:00 Download a20ef4e
Download 69c59e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-03T08:10:04+01:00 Download 3d20833
Download 3d20833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 8 2019-11-30T03:11:50+01:00
Download e8cb7b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 8 2019-12-01T13:18:17+01:00
Download 71125bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:54:21+01:00 Download 1c2d543
Download 2c75063 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:51:18+01:00 Download 58b3f67
Download 25cb7ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:40:22+01:00 Download baab39d

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

Trying to find witnesses for program (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 28 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 04bee90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T01:15 CET (sv-comp)
Download d1eccfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:51:50
Download 807f500 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T10:20:10+01:00
Download 83674fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T12:21:23+01:00
Download 0214969 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T02:07 CET (sv-comp)
Download 08b4d26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T07:05:45
Download 5427feb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2018-12-07T12:34 CET (sv-comp)
Download 126f614 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-07T10:41:28+01:00
Download f89077f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:23:32+01:00 Download c79e2d9
Download 39d7fe4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:53:05+01:00 Download 2d3dfd9
Download eaf73f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:37:14+01:00 Download b602086
Download eaa06c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:25:41+01:00 Download d05265c
Download 0876e2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T18:21:06+01:00 Download 428292c
Download 8de8627 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:44:03+01:00 Download 0214969
Download a90a3c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T22:10:09+01:00 Download 08b4d26
Download c82bef5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T08:32:27+01:00 Download 126f614
Download 782ce70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T04:51:30+01:00 Download c7f5634
Download 7c7292d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:42:33+01:00 Download 469c628
Download 06f896d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T18:46:44+01:00 Download 1f7cfa6
Download a9614eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:44:51+01:00 Download 5427feb
Download 55cf9ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T10:18:00+01:00 Download 0954f5c
Download 5012ed7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:47:55+01:00 Download 9e51651
Download 117971d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:19:48+01:00 Download e3ac2d1
Download 6e9d045 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:09:58+01:00 Download 6442651
Download 9e51651 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-05T08:04:49+01:00
Download 38f9f45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:38:02+01:00 Download ed1db0f
Download 45b780a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:08:32+01:00 Download 2d3d1c0
Download a766fba Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:21 CET (sv-comp)

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

Trying to find witnesses for program (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 23 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download feb2d82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2017-12-03T07:43Z
Download 207114f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:36 CET (sv-comp)
Download 0986a0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2017-12-03T10:34Z
Download b0bd95f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 5 2017-12-01T13:20 CET (sv-comp)
Download 9a766aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:26:17+01:00
Download c8c3577 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:18Z
Download d7e1a43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:15 CET (sv-comp)
Download 3535953 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 7 Sun Dec 3 00:10:26 2017
Download 42fd283 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 4 2017-12-03T03:53 CET (sv-comp)
Download 633528a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 8 2017-12-03T05:19Z
Download 9448bbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T12:21 CET (sv-comp)
Download acddf27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T21:14 CET (sv-comp)
Download 30c5955 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 8 2017-12-02T16:54Z
Download d194f0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T04:49:29.724241
Download d22c919 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T09:12:43.199789
Download 897763c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T15:43 CET (sv-comp)
Download 36cd6ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-11-30T17:55 CET (sv-comp)
Download f5f2d66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 8 2017-11-30T22:51:59+01:00
Download 5201e7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T14:47:53+01:00
Download fd5e4a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T20:40:26+01:00
Download 222c156 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T21:08:17+01:00
Download 1da28f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 7 2017-11-30T20:20 CET (sv-comp)
Download 1dea5a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 8 2017-12-02T18:39Z

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

Trying to find witnesses for program (07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956, sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c, 07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/07f4808a529c009f57a881d7b1897a8e79ad8d178f7a6b3c25d05d1beb7c0956.json

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