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-cdfpl/sine_1_false-unreach-call_true-termination.i
programSHA 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
witnessName results-validated/cpa-seq-validate-violation-witnesses-utaipan.2018-12-09_2052.logfiles/sv-comp19_prop-reachsafety.sine_1_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA c3ff84978b81fb2a291e80f320f23cb46dfe24815dd788e3d674a80370b58cc4

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T20:54:37+01:00
inputwitnesshash 30ffd9dde8c77fa89c0b08d75c314080b95dbb88227e178d29c4daff34680987
producer CPAchecker 1.7-svn 29852
program-sha256 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
programfile ../../sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i
programhash 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c3ff84978b81fb2a291e80f320f23cb46dfe24815dd788e3d674a80370b58cc4.graphml
witness-sha256 c3ff84978b81fb2a291e80f320f23cb46dfe24815dd788e3d674a80370b58cc4
witness-size 3879
witness-type correctness_witness

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

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

Trying to find witnesses for program (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.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 (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.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 (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.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 (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.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 (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 19 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 13ec7e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-03T22:55 CET (comp)
Download 6157a01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:54:53+01:00 Download 15d0929
Download 2ca76bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:58:11+01:00 Download 13ec7e1
Download 51cf581 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:57:00+01:00 Download b1a8cd7
Download 929a69f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:08:07+01:00 Download 5319ff0
Download 5319ff0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 5 2019-11-30T02:58:03+01:00
Download d65ca09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 3 2019-12-07T14:46:08+01:00
Download 15d0929 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T06:19:06+01:00
Download 3dbfc18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness BRICK 4 2019-12-07T21:41:01Z
Download 3446828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T21:09:44+01:00 Download 1c757f2
Download d09a70c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:54:21+01:00 Download 28e0668
Download 4592fcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:44:53+01:00 Download dfd3973
Download 28b6d4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T01:52:41+01:00 Download d65ca09
Download bfb9ad6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:28:36+01:00 Download ac57e41
Download a2a4b9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:50:58+01:00 Download 3dbfc18
Download 88e8d9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T21:19:08+01:00 Download fc39849
Download 7a645af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T20:20:14+01:00 Download 4e4da9c
Download 2839eef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:35:42+01:00 Download c997cb6
Download 0ddecef Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:17 CET (comp)

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

Trying to find witnesses for program (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 19 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download edf729c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T10:22:07
Download ae57c8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-07T07:47 CET (sv-comp)
Download 59e6cbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 4 2018-12-10T19:05:22+01:00
Download 8a44ebe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T09:35:21+01:00
Download 4b984f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:02:40+01:00 Download dc65caa
Download bb7b5a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:53:17+01:00 Download 8a44ebe
Download f1bf7f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T18:47:31+01:00 Download 837ceeb
Download a817705 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:28+01:00 Download c3056df
Download a088cb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:04:59+01:00 Download e53b8e9
Download c3056df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T01:45:30+01:00
Download 02a626e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:38:10+01:00 Download 59e6cbc
Download c3ff849 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:54:37+01:00 Download 30ffd9d
Download 4512a2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:37:56+01:00 Download 9e6ebc4
Download 3ff4a1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:02:56+01:00 Download 2943629
Download b37be4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:45:11+01:00 Download ae57c8a
Download 14ea3ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T10:17:51+01:00 Download 5c8ea95
Download 53c2983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:43:23+01:00 Download 19068fa
Download 7a755c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:05:05+01:00 Download 1fd984c
Download eef2fc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T01:05 CET (sv-comp)

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

Trying to find witnesses for program (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 17 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3b62638 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-02T19:01Z
Download a473367 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T04:35:05.410955
Download 52d4cc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T12:55:39.243413
Download dae702a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T18:06 CET (sv-comp)
Download 0de8a0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T19:27 CET (sv-comp)
Download a74fbb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-03T01:13:56+01:00
Download 7a645da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T15:41:19+01:00
Download 3e1eb72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T16:24:04+01:00
Download 0af6dd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T23:42:43+01:00
Download ff8ab0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T06:07:27+01:00
Download d7df575 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-12-01T02:57 CET (sv-comp)
Download 4efdc9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T07:36Z
Download 18bc520 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-12-01T02:57 CET (sv-comp)
Download e19962a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:11:13.302285
Download bc02f38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:07:15.059202
Download e9f8095 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T13:21 CET (sv-comp)
Download 314b36b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T16:16 CET (sv-comp)

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

Trying to find witnesses for program (1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514, sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_1_false-unreach-call_true-termination.i, 1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1557390de6fc722bb394b13105554fca7649fc2caceeb072bd2f994729cf3514.json

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