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/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c
programSHA 096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00
witnessName results-verified/divine-smt.2018-12-06_1106.logfiles/sv-comp19_prop-reachsafety.Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c.files/witness.graphml
witnessSHA 15a1d620b72ec1dfd0aceae478892632bf41c874e0bfb1c71719a9d06341138c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T23:19 CET (sv-comp)
memorymodel precise
producer DIVINE 4
programfile ../../sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c
programhash d3562c726fb0df5872bc6ae08c11ec0d40862c19
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/15a1d620b72ec1dfd0aceae478892632bf41c874e0bfb1c71719a9d06341138c.graphml
witness-sha256 15a1d620b72ec1dfd0aceae478892632bf41c874e0bfb1c71719a9d06341138c
witness-size 3406
witness-type violation_witness

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

Trying to find witnesses for program (096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00, sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c).

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

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

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

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

Found 12 witnesses for program sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c, 096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0c063cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 8 2019-11-30T14:47:58+01:00
Download 89b1ee1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 8 2019-12-01T10:54:08+01:00
Download 7be82ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 01:23:16
Download 1bce103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-11T21:57:41+01:00 Download d5d780f
Download c6269f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-11T21:09:47+01:00 Download 7be82ef
Download a871c92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-11T20:44:49+01:00 Download 9d7ac15
Download 7585daa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-03T08:56:54+01:00 Download 5b4326c
Download c55b7a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 28 2019-12-03T08:10:40+01:00 Download 9d5e9c5
Download 9d5e9c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 28 2019-11-30T03:27:34+01:00
Download d5d780f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 28 2019-12-01T08:04:11+01:00
Download 5565f20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:55:31+01:00 Download 7ccc2f2
Download 568f4d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:52:19+01:00 Download c15429b

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

Trying to find witnesses for program (096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00, sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c, 096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 54feca6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:08:57
Download 55c8e98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-07T12:07:48+01:00
Download ce4201e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-05T23:17:04+01:00
Download 773ff66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T16:24 CET (sv-comp)
Download 726ffcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T06:08:24
Download e2cbbab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 17 2018-12-06T22:46 CET (sv-comp)
Download a19a61f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 28 2018-12-06T12:47:16+01:00
Download 05176f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-09T21:23:37+01:00 Download b42d06f
Download b1504ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-09T18:21:00+01:00 Download c9a8050
Download e97b6a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-08T23:42:11+01:00 Download 773ff66
Download 27dbbf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-08T22:09:47+01:00 Download 726ffcf
Download 421f97d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-08T08:09:43+01:00 Download a19a61f
Download 46c055e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-08T04:56:39+01:00 Download e9e57d9
Download aca0ac7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-08T04:01:37+01:00 Download 15a1d62
Download 0ed57b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-06T09:49:12+01:00 Download 39de8dc
Download 39de8dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 28 2018-12-05T21:12:29+01:00
Download e7eab4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:36:01+01:00 Download da38d0a
Download d2fa9c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:09:37+01:00 Download 89070a4

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

Trying to find witnesses for program (096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00, sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c).

Found 19 witnesses for program sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c, 096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f6590c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 10 2017-12-03T07:44Z
Download eca90c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 8 2017-12-01T14:37 CET (sv-comp)
Download 1725ee9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T11:34:48+01:00
Download 5f9e1c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 18 Sat Dec 2 19:22:49 2017
Download a0a5cb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 25 2017-12-03T02:07Z
Download e7f4a9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T03:07 CET (sv-comp)
Download f7ca75c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:00 CET (sv-comp)
Download c1abf04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 25 2017-12-02T11:54Z
Download bf87d50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T19:50:45.395058
Download be85038 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T10:40:24.375464
Download 898640b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 27 2017-12-01T03:52:13+01:00
Download ea1cd63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T14:00:15+01:00
Download 9d9c7b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T20:54:35+01:00
Download 3dfd7cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T11:19:31+01:00
Download 590a87b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 18 2017-12-01T02:58 CET (sv-comp)
Download 14375d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 25 2017-12-02T20:53Z
Download 7114c29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-12-01T18:36 CET (sv-comp)
Download 876378e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-11-30T20:12 CET (sv-comp)
Download 56b4a6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:32:26+01:00 f7817a2

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

Trying to find witnesses for program (096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00, sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c, 096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/096d5f6a756a0beb96c5e3d1ef03309ca7fd94e559854024f151c3b1f05f0b00.json

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