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_20_true-unreach-call.c
programSHA 91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98
witnessName results-validated/cpa-seq-validate-correctness-witnesses-cbmc.2018-12-06_0735.logfiles/sv-comp19_prop-reachsafety.fibo_20_true-unreach-call.c.files/witness.graphml
witnessSHA ae99718cdc8259d6d1557928267a0b970b23adaff90db6548c3613e0448c076f

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T08:27:14+01:00
inputwitnesshash 241823a8196cd698ec8243187fb7fb81b3843ac9acac346d97eaa4fa9d675d3b
producer CPAchecker 1.7-svn 29852
program-sha256 91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98
programfile ../../sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c
programhash 91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ae99718cdc8259d6d1557928267a0b970b23adaff90db6548c3613e0448c076f.graphml
witness-sha256 ae99718cdc8259d6d1557928267a0b970b23adaff90db6548c3613e0448c076f
witness-size 6018
witness-type correctness_witness

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

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

Trying to find witnesses for program (91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98, sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c).

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

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

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

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

Found 12 witnesses for program sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c, 91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ed472c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:06 CET (comp)
Download abf4938 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:27:56+01:00 Download 6a0be22
Download bf87199 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:08:41+01:00 Download dfa9dd1
Download 08509ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:16+01:00 Download f3d8a1a
Download ce5b590 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:51:47+01:00 Download 5c3a722
Download a0fa104 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T02:14:44+01:00 Download fc7573e
Download 24dbb09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:12:53+01:00 Download f475cc8
Download fd2d1db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:28+01:00 Download ed472c1
Download 80b5c2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T19:03:29+01:00 Download 0ec4be8
Download 6145b17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T16:19:12+01:00 Download 7af3ae2
Download 7af3ae2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T07:15:52+01:00
Download dfa9dd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T00:29:23+01:00

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

Trying to find witnesses for program (91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98, sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c).

Found 17 witnesses for program sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c, 91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c7ce7d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:07 CET (sv-comp)
Download de181a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T19:17:53
Download 3af9b56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T23:56 CET (sv-comp)
Download 0605df7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-08T02:15:29+01:00
Download 4ff2414 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T19:50:15+01:00 Download 63f0b78
Download 23c191d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T10:30:37+01:00 Download 27fcc53
Download a5bc766 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T21:06:42+01:00 Download 2261ac7
Download 6ac26a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:24:20+01:00 Download c7ce7d8
Download 6e3696d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:41:53+01:00 Download de181a3
Download 37350ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:41:29+01:00 Download 0605df7
Download 85928c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:20:21+01:00 Download 78558ca
Download 4beedba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T02:11:33+01:00 Download 27fcc53
Download bbe854f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:39:04+01:00 Download 3af9b56
Download 22e4b9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:57+01:00 Download 61cbab5
Download 6a33f5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:00:31+01:00 Download e545c9c
Download ae99718 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:27:14+01:00 Download 241823a
Download e545c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T08:22:38+01:00

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

Trying to find witnesses for program (91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98, sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c).

Found 17 witnesses for program sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c, 91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5689a92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T15:40:53+01:00
Download 443f85f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T01:17:14+01:00
Download 74fb043 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T21:20:41+01:00
Download 0117deb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness VIAP 25271 2017-12-03T04:05 CET (sv-comp)
Download e6a42ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T09:29 CET (sv-comp)
Download b7b4cdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T21:11 CET (sv-comp)
Download c6697a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T17:20:44.344063
Download f6d0d80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T13:19:07.433865
Download ea7695c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-01T05:45:32+01:00
Download ae90cdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:22:48+01:00 7d5f570
Download 907e8bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:11:25+01:00 1ad8271
Download 323b978 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T08:11:58+01:00 b9fa5bc
Download 66b4d2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:37:35+01:00 d330428
Download 30800aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:08:43+01:00 7f9bbba
Download 234200d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:12:40+01:00 4a190fe
Download 85b1f51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:03:43+01:00 6772001
Download f90a296 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 12393 2017-11-30T12:36 CET (sv-comp)

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

Trying to find witnesses for program (91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98, sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_20_true-unreach-call.c, 91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/91d61c664a2dc2458a2e211c6a24c238cd2d5bd4a64538d7112eb2ca1fb97d98.json

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