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/floats-cbmc-regression/float_lib2_true-unreach-call.i
programSHA cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
witnessName results-verified/pinaka.2018-12-06_2014.logfiles/sv-comp19_prop-reachsafety.float_lib2_true-unreach-call.i.files/witness.graphml
witnessSHA f842e0708c2af339c7838e0149c29cc1297a4a564d780a9a4c2ff9ba8d7a5e42

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T00:00 CET (sv-comp)
producer Pinaka
program-sha256 cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i
programhash cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/f842e0708c2af339c7838e0149c29cc1297a4a564d780a9a4c2ff9ba8d7a5e42.graphml
witness-sha256 f842e0708c2af339c7838e0149c29cc1297a4a564d780a9a4c2ff9ba8d7a5e42
witness-size 3170
witness-type correctness_witness

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

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

Trying to find witnesses for program (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.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 (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.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 (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.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 (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.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 (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e2c9a6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:22 CET (comp)
Download 3a84537 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:23:00+01:00 Download b61c904
Download ab3da3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:19:05+01:00 Download 386465e
Download e7e9205 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:44+01:00 Download b452e57
Download e8bfcb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:46:23+01:00 Download 3052e69
Download 1b1b9d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:47:42+01:00 Download 9ab5148
Download a971bc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:02:52+01:00 Download f3c0bab
Download 3eb59aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T19:46:18+01:00 Download 2afd087
Download 9395f64 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 5968d6e
Download 786348d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:02:58+01:00 Download 68c1688
Download 779144d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:58+01:00 Download e2c9a6c
Download ad56c1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T16:50:18+01:00 Download 7caa601
Download 7caa601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T11:56:38+01:00
Download 3052e69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 6 2019-12-07T15:51:25+01:00
Download 386465e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T01:57:35+01:00
Download 9ab5148 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:38:29Z

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

Trying to find witnesses for program (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4704e3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:03:38
Download f842e07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T00:00 CET (sv-comp)
Download 8f446f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T21:35:23+01:00
Download 47da4de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:09:29+01:00 Download 3ad2543
Download 9e10392 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:14:23+01:00 Download f5d87aa
Download 2de1e5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T16:56:25+01:00 Download f1b5364
Download f5cb3e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:43:56+01:00 Download 4704e3e
Download e87c939 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:07:49+01:00 Download 8f446f7
Download ab28212 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:00:34+01:00 Download 793d08b
Download 879c0fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:44:14+01:00 Download ded38d9
Download 48e2507 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:25:09+01:00 Download f842e07
Download 6755a84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:19+01:00 Download b80ab46
Download 3642dd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:10:32+01:00 Download bc86aaf
Download 08c6a4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:10:53+01:00 Download 86a0326
Download 6d82503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:00:48+01:00 Download 03b9dec
Download bc86aaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T01:47:11+01:00

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

Trying to find witnesses for program (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 25 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d26038c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-02T08:02:39+01:00
Download 0c19dcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 28 2017-12-02T20:41Z
Download 7b3d3f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 30 2017-12-02T09:30Z
Download c760c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T19:38:20.521327
Download 6e83d44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T19:36:59.080218
Download 93a0acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-12-03T03:21:07+01:00
Download 7995868 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T04:33:40+01:00
Download 22758d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T06:58:01+01:00 659f2d5
Download f83a909 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:03:49+01:00 a087d02
Download a8a519b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T02:56:20+01:00 8fb3a25
Download 9ab0e35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T00:38:21+01:00 63b929f
Download a6c796f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T08:10:18+01:00 930b0b5
Download b7008eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:34:11+01:00 0cda3ef
Download b8ce20e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:13:55+01:00 386df77
Download f64abf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:34:48+01:00 27a3915
Download 6c84240 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:54:15+01:00 893eaae
Download 94a94bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:29:24+01:00 9a41648
Download 566029f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:10:25+01:00 92074bc
Download d1c82e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T04:53:25+01:00 4c6dba7
Download a61b1fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T16:11:25+01:00
Download ca1e1a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 20 2017-11-30T15:22:37+01:00
Download e7037a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T12:42:37+01:00
Download 98bca6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 8 2017-11-30T16:42 CET (sv-comp)
Download 0f80ae8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 28 2017-12-02T13:48Z
Download 0e16001 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 66 2017-12-01T00:42 CET (sv-comp)

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

Trying to find witnesses for program (cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138, sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float_lib2_true-unreach-call.i, cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/cde6358327d85b32f8bfe6e3cfb84325c6831cf838dbc00458b73fbbaaffd138.json

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