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/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c
programSHA 635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c.files/witness.graphml
witnessSHA c9b514fc7c56e1e713b090ff2bdae28390293df014263082fa48c07626e0f069

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T05:19:11+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315
programfile ../../sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c
programhash 635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c9b514fc7c56e1e713b090ff2bdae28390293df014263082fa48c07626e0f069.graphml
witness-sha256 c9b514fc7c56e1e713b090ff2bdae28390293df014263082fa48c07626e0f069
witness-size 21290
witness-type correctness_witness

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

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

Trying to find witnesses for program (635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315, sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c).

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

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

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

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

Found 9 witnesses for program sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c, 635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a692dfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 39 2019-12-04T01:05 CET (comp)
Download 46a5998 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 57 2019-12-11T21:50:24+01:00 Download b046554
Download 6524bd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 68 2019-12-11T20:44:49+01:00 Download 69995ab
Download 486d6a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 57 2019-12-04T02:58:25+01:00 Download a692dfe
Download 4b2a894 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 57 2019-12-03T08:10:34+01:00 Download 1bef545
Download 1bef545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 56 2019-11-30T00:05:12+01:00
Download b046554 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 56 2019-12-01T03:01:20+01:00
Download f82acdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-11T20:54:51+01:00 Download 05f7853
Download 9b799fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-05T19:34:10+01:00 Download 68dd07e

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

Trying to find witnesses for program (635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315, sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c).

Found 7 witnesses for program sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c, 635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0f5e131 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T06:09 CET (sv-comp)
Download d9b9200 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T12:47:52
Download c9b514f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 21 2018-12-07T05:19:11+01:00
Download e875f68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 21 2018-12-08T06:48:49+01:00 Download c9b514f
Download a51fd34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T08:29:04+01:00 Download 107cc8b
Download 3d0bd03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-05T13:12:25+01:00
Download f95e2b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T13:26 CET (sv-comp)

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

Trying to find witnesses for program (635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315, sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c).

Found 26 witnesses for program sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c, 635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7d0b9d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 22 2017-12-02T10:19:01+01:00
Download 2306c41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 31 2017-12-02T17:33Z
Download 2e88a97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-01T23:31 CET (sv-comp)
Download 6e76fbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:00:26.444598
Download 768e75f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:43:07.038278
Download fb8ba37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T22:40:36.108315
Download cecec96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T15:59:19.263320
Download 71e6007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 35 2017-12-01T18:51 CET (sv-comp)
Download 9a9098b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 20 2017-12-02T19:42:47+01:00
Download 323d3a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T17:18:56+01:00
Download 5a93b36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-03T07:04:23+01:00 5d93e2f
Download f2fcb00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 20 2017-12-03T04:21:48+01:00 8a4fc9a
Download 4fbe4b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-03T01:22:07+01:00 5584cb3
Download 44b4499 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-02T20:02:53+01:00 8f652f3
Download 5f6ccbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-02T09:08:24+01:00 049f6b3
Download 3723fb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T22:41:03+01:00 71e7622
Download af4165d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T08:26:06+01:00 7ee34a8
Download c93c495 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T06:52:37+01:00 df28230
Download 549820b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T06:10:21+01:00 6e63ecd
Download ac333d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T05:19:07+01:00 29cd113
Download d175a42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-11-30T15:30:17+01:00
Download a609970 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 316 2017-11-30T13:49 CET (sv-comp)
Download b0ac859 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 31 2017-12-02T19:33Z
Download 4a33c7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 88 2017-11-30T14:24 CET (sv-comp)
Download 6d153cc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 315 2017-12-01T13:06 CET (sv-comp)
Download 50d4fc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 89 2017-12-01T13:52 CET (sv-comp)

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

Trying to find witnesses for program (635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315, sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c, 635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/635163024c035c515c26db9bb9c23fe2c4c42e84a7d695df16b9bfecaa1c4315.json

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