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/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c
programSHA ca6429cd789a67ac8317085768ba9ada2a78d5369a2da6605efa092002e3964f
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-nooverflow.Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c.files/witness.graphml
witnessSHA e7e36be65ce2353e4ad59e1c9d0c2d32a42ac4672a33506e73076305955439da

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T10:25:20+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 ca6429cd789a67ac8317085768ba9ada2a78d5369a2da6605efa092002e3964f
programfile ../../sv-benchmarks/c/recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c
programhash ca6429cd789a67ac8317085768ba9ada2a78d5369a2da6605efa092002e3964f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/e7e36be65ce2353e4ad59e1c9d0c2d32a42ac4672a33506e73076305955439da.graphml
witness-sha256 e7e36be65ce2353e4ad59e1c9d0c2d32a42ac4672a33506e73076305955439da
witness-size 8766
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7c8235a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 8 2019-11-29T21:57:53+01:00
Download 557d64c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 8 2019-12-01T04:56:57+01:00
Download 282eda7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T23:45:20+01:00 Download 958839c
Download c77f34c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T19:45:19+01:00 Download 305e9ac

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a463ce9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:27:43
Download e7e36be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-07T10:25:20+01:00
Download 566ac87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T05:46:32+01:00
Download af4d6e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:15:15
Download 3c98acc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:04:33+01:00 Download fef419a
Download 96c78d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T21:06:22+01:00 Download 822134a
Download 8c0b2fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:29:43+01:00 Download 134070c
Download 5c46f9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:09:55+01:00 Download 83963b3
Download 2159d9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T21:48:17+01:00 Download af4d6e4
Download 3f17325 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:28:16+01:00 Download e40acd4

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download aa76724 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 11 2017-12-03T07:44Z
Download 24021d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 8 2017-12-01T13:57 CET (sv-comp)
Download 7327321 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T10:53:23+01:00
Download 395694b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T19:49:24+01:00
Download 85c7a02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T12:24:27+01:00
Download 8ccd69e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T11:06:26+01:00
Download 594821c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 9 2017-12-02T23:16Z
Download 0c8f775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-12-01T18:09 CET (sv-comp)
Download f6a430a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-12-01T07:12 CET (sv-comp)
Download cd2ec02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T06:50:43+01:00 336cd60
Download 04bb908 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T00:37:09+01:00 b3be754
Download da05a02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:13:54+01:00 b5ca2a1
Download b98707a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 9 2017-12-02T10:00Z

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

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

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

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