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_2_false-unreach-call_true-termination.c
programSHA 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.fibo_2calls_2_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 8c3410151bff845fa9f940ab534ab0a2c0afd232eff0e82836cd275c6bebf72e

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8c3410151bff845fa9f940ab534ab0a2c0afd232eff0e82836cd275c6bebf72e.json

Key Value
architecture 32bit
creationtime 2017-12-01T03:07 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
programfile /tmp/vcloud-vcloud-master/worker/working_dir_7c830228-a49f-4a00-b22d-7ff3b9a717b2/sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c
programhash 0d7907681604b1ce9d21af31806cc60e045b313d
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/8c3410151bff845fa9f940ab534ab0a2c0afd232eff0e82836cd275c6bebf72e.graphml
witness-sha256 8c3410151bff845fa9f940ab534ab0a2c0afd232eff0e82836cd275c6bebf72e
witness-size 4650
witness-type violation_witness

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

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

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

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

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

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

Found 18 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 18377d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 00:27:13
Download 86f2b29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2019-12-03T23:33 CET (comp)
Download 95adc82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:42:49+01:00 Download 34ed61b
Download 2a58904 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:39:10+01:00 Download 6cb2ea9
Download a90e39d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:09:17+01:00 Download 18377d7
Download f98ceaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:54:21+01:00 Download 18c63bd
Download 06b257e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:44:44+01:00 Download 6cd14c1
Download 638b101 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:27:00+01:00 Download bd5ec78
Download 328ef21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T21:16:47+01:00 Download e71bf50
Download 46f464f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-06T02:38:03+01:00 Download abc1a56
Download c8ada11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-04T02:58:17+01:00 Download 86f2b29
Download 877fae7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-03T08:57:03+01:00 Download 138a206
Download 7b65af8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-03T08:08:36+01:00 Download a4600a5
Download a4600a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 8 2019-11-30T12:13:40+01:00
Download 34ed61b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 8 2019-12-01T00:31:04+01:00
Download 2b8442a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T01:51:17+01:00 Download 0810c10
Download fd79ab4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T20:20:22+01:00 Download a6c40f2
Download de9b522 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:25 CET (comp)

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

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

Found 26 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2c3e065 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T00:42 CET (sv-comp)
Download 558cd67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T03:44:40
Download 4066930 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 7 2018-12-06T22:53 CET (sv-comp)
Download 65cee7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-08T00:39:08+01:00
Download 497d369 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-10T10:48:41+01:00 Download 9d5dc5d
Download b548f65 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 e65c164
Download 34b10e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:29:52+01:00 Download 55e468b
Download bfc4f00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T18:20:43+01:00 Download 12e04a3
Download c0b64b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:43:39+01:00 Download 2c3e065
Download c6b1fce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T22:11:14+01:00 Download 558cd67
Download a900738 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T08:57:30+01:00 Download 65cee7d
Download 683c069 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T05:03:15+01:00 Download 6ef8b72
Download ab23555 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T04:37:06+01:00 Download 9d5dc5d
Download 6652e86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T18:47:49+01:00 Download fd03b64
Download 7118027 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:43:00+01:00 Download 4066930
Download f605968 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T01:16:28+01:00 Download 10e7d7f
Download 33342ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T10:14:21+01:00 Download c8b2395
Download 614bd97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:48:57+01:00 Download 4a294a7
Download 4a294a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-05T07:51:30+01:00
Download 4625c30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:37:51+01:00 Download 6ced7f5
Download 8649a86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:53:10+01:00 Download acb9fc8
Download 9a81028 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:37:18+01:00 Download c4e70fa
Download 8176170 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:19:26+01:00 Download 4417557
Download 2ee626d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:19:05+01:00 Download 277a773
Download f38cfbe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:49 CET (sv-comp)
Download 3299cc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T03:52 CET (sv-comp)

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

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

Found 20 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6ac115e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:36 CET (sv-comp)
Download 0c17191 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 6 Sat Dec 2 17:31:54 2017
Download e65c164 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 7 2017-12-03T04:01 CET (sv-comp)
Download 056be1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 9 2017-12-03T05:06Z
Download 784c826 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:53 CET (sv-comp)
Download 6f593d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 5 2017-12-01T21:44 CET (sv-comp)
Download 8c830b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 9 2017-12-02T01:40Z
Download 1be896e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T19:31:13.120774
Download e72b26a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T09:22:52.221007
Download 8a65a84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T18:58 CET (sv-comp)
Download 8c34101 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T03:07 CET (sv-comp)
Download 171f84e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 8 2017-11-30T17:46:28+01:00
Download 63bea5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 14 2017-12-01T00:10:47+01:00
Download 7dff649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 8 2017-11-30T19:17:29+01:00
Download 38459e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 8 2017-12-01T21:51:06+01:00
Download e2dc3b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 6 2017-11-30T18:42 CET (sv-comp)
Download 957afce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 9 2017-12-02T19:07Z
Download 6d76136 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:28:58.258544
Download 6dfcee6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:26:56.082634
Download e367b64 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T13:53 CET (sv-comp)

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

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

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

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