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/float11_true-unreach-call_true-termination.i
programSHA ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776
witnessName results-validated/cpa-seq-validate-correctness-witnesses-ukojak.2018-12-09_1935.logfiles/sv-comp19_prop-reachsafety.float11_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 52c1fdcce90c3a5b3c123ae730f56c7df0282d57f969c812c11f791254d870b4

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T19:54:12+01:00
inputwitnesshash 575b9822952e10aaaefbaf3315f1ee8c256cfa385858088c81b052cd273c5794
producer CPAchecker 1.7-svn 29852
program-sha256 ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i
programhash ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/52c1fdcce90c3a5b3c123ae730f56c7df0282d57f969c812c11f791254d870b4.graphml
witness-sha256 52c1fdcce90c3a5b3c123ae730f56c7df0282d57f969c812c11f791254d870b4
witness-size 4616
witness-type correctness_witness

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

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

Trying to find witnesses for program (ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776, sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i).

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i, ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776.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 '19

Trying to find witnesses for program (ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776, sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i).

Found 23 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i, ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b1ca248 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T00:20 CET (sv-comp)
Download 223293e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T14:11:52
Download c1e0443 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:02 CET (sv-comp)
Download 9abea39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T23:00:48+01:00
Download fbf11c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:04:04+01:00 Download 8859590
Download 6981b3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:30+01:00 Download f4edfec
Download d6cae26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:19:33+01:00 Download 42de8a3
Download 52c1fdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:54:12+01:00 Download 575b982
Download 975d45f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:13:34+01:00 Download ef58882
Download fc6fd16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:09:20+01:00 Download b1ca248
Download e1b7ded Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:37:14+01:00 Download 223293e
Download eb07a59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:44:27+01:00 Download 9abea39
Download 8aba2b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:12:43+01:00 Download 633b5b0
Download 2640dd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:13:30+01:00 Download f4edfec
Download dcea1dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:43:13+01:00 Download cfcd835
Download 9261ad7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:39:31+01:00 Download c1e0443
Download 1f284c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:29+01:00 Download 3f83a1e
Download 0d24ace Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:01:07+01:00 Download 886a8e2
Download dd26ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:27:05+01:00 Download f6f92a8
Download 3cb22c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:11:48+01:00 Download b605f0b
Download 886a8e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T10:09:14+01:00
Download 6fa1664 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T05:45 CET (sv-comp)
Download 06b85d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T06:12 CET (sv-comp)

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

Trying to find witnesses for program (ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776, sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i).

Found 35 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i, ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cfcd835 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:08 CET (sv-comp)
Download 60c538f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 26 2017-12-03T02:05Z
Download 0f08980 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T02:03 CET (sv-comp)
Download b7a8080 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 26 2017-12-02T15:03Z
Download 619c174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:01:08.401267
Download 70d6d0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:35:07.730880
Download c0c0227 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T20:28:38.140703
Download d4b7e00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T07:51:59.747361
Download 8a46b59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 3 2017-12-01T17:46 CET (sv-comp)
Download b6c111f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-03T00:01:53+01:00
Download f0a69ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:25:46+01:00
Download 5f38bcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T06:57:55+01:00 7b84f1b
Download 546153a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:26:09+01:00 6493f6b
Download f2e4116 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T03:01:24+01:00 c2a6079
Download 2afafd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:03:55+01:00 8436347
Download ba7bed4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:13:25+01:00 f194e8f
Download 60da3bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T15:11:18+01:00 9c80f88
Download b93d600 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T07:25:42+01:00 28adc64
Download 1250e05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:06:21+01:00 e89305c
Download 6888471 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:37:57+01:00 671e8c5
Download cb4ac3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:52+01:00 ef012ae
Download 84523f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T07:10:36+01:00 01b3fa9
Download 0b247e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:47:37+01:00 67a912c
Download 85fd239 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:16:00+01:00 72ed729
Download 8a5edf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:34:38+01:00 000e2fd
Download 88d2057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:02:24+01:00 363929a
Download d47549b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T21:47:56+01:00
Download f13956a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 8 2017-11-30T12:06:26+01:00
Download f9bba05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T02:51:42+01:00
Download 295af45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T07:45:10+01:00
Download 945ba1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 10 2017-12-01T00:02 CET (sv-comp)
Download 11191d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 26 2017-12-02T18:42Z
Download 046fc9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 12 2017-12-01T03:47 CET (sv-comp)
Download 86d4d5a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 10 2017-12-01T13:06 CET (sv-comp)
Download 674338b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 12 2017-12-01T12:58 CET (sv-comp)

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

Trying to find witnesses for program (ef017dda202afe870457a9bfe8660e0648478f057409b8f744198158566b4776, sv-benchmarks/c/floats-cbmc-regression/float11_true-unreach-call_true-termination.i).

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

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