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 (0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79, sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c).

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

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

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

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

Found 17 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c, 0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1dfd939 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 21:49:38
Download 57451cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 25 2019-12-03T22:40 CET (comp)
Download c95c420 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 43 2019-12-11T21:59:49+01:00 Download f4e4e22
Download 3540a80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 43 2019-12-11T21:09:02+01:00 Download 1dfd939
Download d60292b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 43 2019-12-11T20:54:24+01:00 Download 0b8a8ae
Download 98e1153 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 43 2019-12-11T20:44:41+01:00 Download 4755ad5
Download d1ca345 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 43 2019-12-06T02:41:24+01:00 Download a8f5710
Download fc41871 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 44 2019-12-04T02:58:44+01:00 Download 57451cb
Download 7dc2ef8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 43 2019-12-03T08:56:49+01:00 Download dd2cef2
Download 63f7d47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 43 2019-12-03T08:08:21+01:00 Download 048edb3
Download 048edb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 43 2019-11-29T14:34:32+01:00
Download f4e4e22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 43 2019-11-30T23:33:43+01:00
Download c0b8fd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T01:51:19+01:00 Download 90d416d
Download ae4192d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:26:12+01:00 Download 70e44d2
Download 2d8641b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T21:18:17+01:00 Download 9fa91e2
Download a8252f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T20:21:42+01:00 Download f4dc5c0
Download 33504f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:24 CET (comp)

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

Trying to find witnesses for program (0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79, sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c).

Found 22 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c, 0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a59bb12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T07:51 CET (sv-comp)
Download 058b98a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T03:55:57
Download b14c37b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 27 2018-12-07T09:02 CET (sv-comp)
Download fc02631 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 43 2018-12-07T19:07:30+01:00
Download a27bf80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-10T10:48:43+01:00 Download 2157ff9
Download 4a52552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-09T21:23:37+01:00 Download 988ba6f
Download 46b8b1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-09T18:16:36+01:00 Download 94f9039
Download 8a3df0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-08T23:44:01+01:00 Download a59bb12
Download 9879fa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-08T22:10:00+01:00 Download 058b98a
Download 88c6962 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-08T08:09:32+01:00 Download fc02631
Download 8453ab6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-08T05:01:16+01:00 Download 11dfdbb
Download 0618327 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-08T04:26:18+01:00 Download 2157ff9
Download 5edd8c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 44 2018-12-07T17:45:15+01:00 Download b14c37b
Download b8d4d0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-07T01:23:38+01:00 Download 551a6cb
Download 58ed96f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-06T10:09:21+01:00 Download adc8638
Download a6ab8f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-06T09:48:16+01:00 Download da5beb0
Download da5beb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 43 2018-12-06T07:21:21+01:00
Download 23b4044 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:34:52+01:00 Download dddab60
Download daad78e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:18:36+01:00 Download d83faa4
Download ba13096 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:11:41+01:00 Download c93b1e3
Download e5bf4cc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T06:49 CET (sv-comp)
Download 84451d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T23:56 CET (sv-comp)

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

Trying to find witnesses for program (0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79, sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c, 0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 971a9d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 21 Sat Dec 2 17:18:07 2017
Download 988ba6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 32 2017-12-03T04:06 CET (sv-comp)
Download 5198998 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 42 2017-12-03T03:11Z
Download 931a19a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T02:19 CET (sv-comp)
Download 147b192 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 5 2017-12-01T20:01 CET (sv-comp)
Download 726262a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T21:00:02.539681
Download 8b3fa95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T08:37:19.373741
Download f39d55a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 10 2017-12-01T20:45 CET (sv-comp)
Download 04ca515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 10 2017-11-30T17:05 CET (sv-comp)
Download e4fc334 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 41 2017-11-30T20:45:57+01:00
Download 07a1d3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 16 2017-11-30T21:10:56+01:00
Download c5fd88d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 8 2017-12-01T01:58:45+01:00
Download 9d3f886 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 9 2017-12-02T03:31:10+01:00
Download e3f9dbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 22 2017-12-01T02:09 CET (sv-comp)
Download c942fe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 42 2017-12-02T03:47Z
Download 865c994 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:21:58.724505
Download 6309fd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:50:02.301519
Download 3ac60e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 20 2017-12-01T16:40 CET (sv-comp)

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

Trying to find witnesses for program (0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79, sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c, 0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0fe40a12d376eb2d8b2618dd68ca56408d6fc4b6ec25baeda44435bd320a9a79.json

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