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_2calls_6_true-unreach-call_true-termination.c
programSHA fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662
witnessName results-validated/cpa-seq-validate-correctness-witnesses-esbmc-kind.2018-12-08_0216.logfiles/sv-comp19_prop-reachsafety.fibo_2calls_6_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA fcadf7e01f870aa7aa52904309cfbc09129fab8e69a9f58cc54ab676c4b198c5

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/fcadf7e01f870aa7aa52904309cfbc09129fab8e69a9f58cc54ab676c4b198c5.json

Key Value
architecture 32bit
creationtime 2018-12-08T04:10:45+01:00
inputwitnesshash 1427ed476149b2df44973c7592d55620e9ac3e13e310179bbc807297f547800c
producer CPAchecker 1.7-svn 29852
program-sha256 fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662
programfile ../../sv-benchmarks/c/recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c
programhash fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/fcadf7e01f870aa7aa52904309cfbc09129fab8e69a9f58cc54ab676c4b198c5.graphml
witness-sha256 fcadf7e01f870aa7aa52904309cfbc09129fab8e69a9f58cc54ab676c4b198c5
witness-size 9082
witness-type correctness_witness

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

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

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

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

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

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

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

Found 15 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c, fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ebd0854 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:37 CET (comp)
Download b53a98a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:29:41+01:00 Download 920135c
Download 8e6d0de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:18:53+01:00 Download 353ce30
Download 00cd1ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:02:30+01:00 Download 8d39dbe
Download b0dbff3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:36:26+01:00 Download a9207c2
Download 669f06d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T23:39:18+01:00 Download be9719a
Download 828ed7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T19:44:07+01:00 Download 5138f87
Download c5216d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-06T02:12:20+01:00 Download 14e425e
Download 59b76d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:13:33+01:00 Download d8f50f2
Download 49d98f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-04T02:07:30+01:00 Download ebd0854
Download adb25e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-11-30T19:55:45+01:00 Download 457bf9b
Download 944da05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-11-30T16:41:58+01:00 Download 245e83e
Download 245e83e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 9 2019-11-30T05:40:56+01:00
Download 353ce30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 9 2019-12-01T03:28:14+01:00
Download feb010e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:39 CET (comp)

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

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

Found 21 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c, fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2731a13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T02:55 CET (sv-comp)
Download 0737471 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:17:47
Download 6e5677f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T22:26 CET (sv-comp)
Download f23bd8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-08T00:21:11+01:00
Download 682a5bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T19:54:41+01:00 Download 1afd4c6
Download 94a5ff0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T10:31:10+01:00 Download e0795c6
Download 7b5bff9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:06:42+01:00 Download b7b35d7
Download 7f34399 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:29:15+01:00 Download 711af4a
Download 46151a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T17:38:26+01:00 Download 359ace7
Download 1c425fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:08:27+01:00 Download 2731a13
Download b1c6c8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T21:29:34+01:00 Download 0737471
Download a687a2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T05:54:31+01:00 Download f23bd8d
Download fcadf7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T04:10:45+01:00 Download 1427ed4
Download 4947508 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:07:53+01:00 Download e0795c6
Download 0a60a50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T16:23:53+01:00 Download 6e5677f
Download 3206c75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:28:59+01:00 Download 4ffc682
Download b19a26a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T08:45:28+01:00 Download a7702c1
Download 629e15a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T08:28:59+01:00 Download 95adae0
Download a7702c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T07:00:54+01:00
Download 16ee628 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:44 CET (sv-comp)
Download 3b585f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T15:40 CET (sv-comp)

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

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

Found 29 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c, fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fd84b00f447f0e99282249dd5833f831be4f359c7cba6f2cb688d12fdb947662.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c4b51f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 16 2017-11-30T14:22:17+01:00
Download 8e0b2d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 8 2017-12-01T00:04:36+01:00
Download a390ea7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 9 2017-12-02T12:00:15+01:00
Download b7b35d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness VIAP 32 2017-12-03T03:52 CET (sv-comp)
Download 4b9ed04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 11 2017-12-02T21:13Z
Download 65a5c18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T01:06 CET (sv-comp)
Download 4928dcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 5 2017-12-01T21:12 CET (sv-comp)
Download e4e740b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:32:31.498803
Download b4302d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:34:22.603637
Download 03d05fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T19:45:22.208359
Download 908c2f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T12:38:20.989206
Download 8dd9a92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T19:53 CET (sv-comp)
Download 0692422 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download 8881c80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 10 2017-12-01T05:08:25+01:00
Download 78774a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T06:50:41+01:00 4a9455d
Download b96a019 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T04:22:29+01:00 dbb29b6
Download c48a064 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T04:19:02+01:00 dc146f0
Download cc47970 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T23:47:18+01:00 26f8e42
Download 9bd59ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T19:46:21+01:00 dfdfc57
Download d13683c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T07:28:27+01:00 3c3d2c0
Download b19246c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T22:31:02+01:00 565f606
Download 133f8aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T22:08:50+01:00 ff8445f
Download 7ec8f8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T08:14:07+01:00 83fe7a9
Download b35e7b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T07:04:23+01:00 a6e8df9
Download 841a18c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T05:02:12+01:00 afcbe7c
Download 7e420f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-11-30T18:19:38+01:00
Download 17b54a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 20 2017-11-30T17:22 CET (sv-comp)
Download f7bc10a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 11 2017-12-02T05:49Z
Download 6a9b022 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 20 2017-12-01T14:42 CET (sv-comp)

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

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

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

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