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

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/recursive-simple/fibo_5_false-unreach-call_true-termination.c
programSHA 6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b
witnessName results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.fibo_5_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 4081d2f4fa8b1be04e30fdc619306d6046f395b6a501a39e17b4ad29048f6a62

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T14:36 CET (sv-comp)
producer CBMC
program-sha256 6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b
programfile ../../sv-benchmarks/c/recursive-simple/fibo_5_false-unreach-call_true-termination.c
programhash 9fa59d7f4411ba9a1b89a97ebb9693c6867ac636
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/4081d2f4fa8b1be04e30fdc619306d6046f395b6a501a39e17b4ad29048f6a62.graphml
witness-sha256 4081d2f4fa8b1be04e30fdc619306d6046f395b6a501a39e17b4ad29048f6a62
witness-size 13280
witness-type violation_witness

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

Trying to find witnesses for program (6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b, sv-benchmarks/c/recursive-simple/fibo_5_false-unreach-call_true-termination.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5870289 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 09:31:27
Download 67a660f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 14 2019-12-03T21:45 CET (comp)
Download db2e16a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T21:42:33+01:00 Download c56fe2c
Download 19a9bd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T21:09:19+01:00 Download 5870289
Download 02aee4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T20:54:49+01:00 Download 47ac440
Download a4262f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T20:44:28+01:00 Download 6b345b0
Download ecc87e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-08T00:27:22+01:00 Download 297c94b
Download ae080d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-07T21:18:40+01:00 Download 8a993dc
Download 56763d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-06T02:41:00+01:00 Download 831565c
Download 077c2ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-04T02:58:32+01:00 Download 67a660f
Download e5bc592 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-03T08:57:31+01:00 Download 6ec3edf
Download c6cea37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-03T08:08:21+01:00 Download 71fbca1
Download 71fbca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 27 2019-11-30T11:17:37+01:00
Download c56fe2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 27 2019-12-01T08:25:47+01:00
Download 5311776 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:51:14+01:00 Download e8f0bd9
Download 2ec4a8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T20:20:35+01:00 Download 782f0e7
Download 1678f84 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:19 CET (comp)

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

Trying to find witnesses for program (6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b, sv-benchmarks/c/recursive-simple/fibo_5_false-unreach-call_true-termination.c).

Found 24 witnesses for program sv-benchmarks/c/recursive-simple/fibo_5_false-unreach-call_true-termination.c, 6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5f05a9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T09:17 CET (sv-comp)
Download f3603c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T02:29:22
Download fe88f33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 16 2018-12-07T01:19 CET (sv-comp)
Download 3c28de1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 27 2018-12-08T00:33:53+01:00
Download 875325d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-10T10:48:44+01:00 Download 9bc7e8e
Download 818b613 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-09T21:23:30+01:00 Download 1e3a115
Download 309a40f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-09T20:53:22+01:00 Download 2b5c163
Download 2dc95b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-09T20:36:16+01:00 Download a820a0f
Download 1c271e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-09T18:21:50+01:00 Download ba3ade6
Download ac467ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-08T23:42:06+01:00 Download 5f05a9b
Download c87bab1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-08T22:11:34+01:00 Download f3603c2
Download ff76432 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-08T08:51:25+01:00 Download 3c28de1
Download 1f24a9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-08T04:59:53+01:00 Download bf00ed4
Download e4014b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-08T04:35:37+01:00 Download 9bc7e8e
Download af8aa90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-07T17:45:27+01:00 Download fe88f33
Download 9f69e5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-07T01:05:04+01:00 Download fda508a
Download 70bf7be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-06T10:17:03+01:00 Download bf87e03
Download 6fa2ed9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-06T09:48:22+01:00 Download e9f2113
Download 3c5bfa9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-06T09:13:52+01:00 Download da553f1
Download e9f2113 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-05T17:08:33+01:00
Download fa0327b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:35:19+01:00 Download c4c6a3e
Download 6910dc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:00:22+01:00 Download e467955
Download a3c8e11 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:44 CET (sv-comp)
Download 5bb4ced Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T07:47 CET (sv-comp)

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

Trying to find witnesses for program (6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b, sv-benchmarks/c/recursive-simple/fibo_5_false-unreach-call_true-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download caf18a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 13 Sun Dec 3 00:06:29 2017
Download 1e3a115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 20 2017-12-03T03:58 CET (sv-comp)
Download a35336b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 24 2017-12-02T23:01Z
Download 23d39f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T15:56 CET (sv-comp)
Download dff82a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 4 2017-12-01T19:53 CET (sv-comp)
Download 50f87c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T15:36:45.784611
Download 3d72c50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T10:30:19.638922
Download 45d28ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 7 2017-12-01T16:59 CET (sv-comp)
Download 49e0cb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 7 2017-12-01T07:24 CET (sv-comp)
Download 6d56b0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 26 2017-11-30T21:39:36+01:00
Download 2883337 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T20:54:26+01:00
Download da0a6bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T15:54:39+01:00
Download 2e7f685 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T20:43:50+01:00
Download 4081d2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 13 2017-11-30T14:36 CET (sv-comp)
Download d3dc81e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 24 2017-12-02T08:45Z
Download 00bd9ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:20:17.399178
Download fdafe0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:18:17.622981
Download f8d0331 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 12 2017-12-01T17:03 CET (sv-comp)

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

Trying to find witnesses for program (6f2849a9277bf9b760deef5192a76a9718e1a67307bc9a3de4db60ddd1a2d51b, sv-benchmarks/c/recursive-simple/fibo_5_false-unreach-call_true-termination.c).

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

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