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/float-benchs/inv_square_int_true-unreach-call_true-termination.c
programSHA edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
witnessName results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.inv_square_int_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 131c4bc291e1d933e7d5493d28d63a02528e6aff8f5d58136deadf9ab506bf9b

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/131c4bc291e1d933e7d5493d28d63a02528e6aff8f5d58136deadf9ab506bf9b.json

Key Value
architecture 32bit
creationtime 2017-12-02T06:12 CET (sv-comp)
producer Symbiotic
program-sha256 edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
programfile /tmp/vcloud-vcloud-master/worker/working_dir_073855e8-35ba-4b64-b0ed-b177a6b827fd/sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c
programhash 0a264ac1dee459017a9965df88403c901cb7750b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/131c4bc291e1d933e7d5493d28d63a02528e6aff8f5d58136deadf9ab506bf9b.graphml
witness-sha256 131c4bc291e1d933e7d5493d28d63a02528e6aff8f5d58136deadf9ab506bf9b
witness-size 764
witness-type correctness_witness

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

Trying to find witnesses for program (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.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 (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.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 (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.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 (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.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 (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c8ec74d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T01:18 CET (comp)
Download a70edaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:24:52+01:00 Download bb13478
Download 1a0b54d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:18:29+01:00 Download f52982e
Download 01eb004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:30+01:00 Download e9270fa
Download 8d6982d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:38:02+01:00 Download a11cef9
Download db1e5a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:48:05+01:00 Download 04462b3
Download 924923d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:30:38+01:00 Download c147081
Download f340b53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:44:32+01:00 Download 360ce5b
Download 1382e83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:12:46+01:00 Download 59c7ac4
Download 19e8ef8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:03:01+01:00 Download 0ba72af
Download 9bcd122 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:35+01:00 Download c8ec74d
Download d39f6a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:10:27+01:00 Download 4940d02
Download 9564d93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T16:30:27+01:00 Download ce6f6f9
Download ce6f6f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T14:50:04+01:00
Download a11cef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T22:22:46+01:00
Download f52982e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T01:28:08+01:00
Download 04462b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:38:34Z

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

Trying to find witnesses for program (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6510a68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T13:48 CET (sv-comp)
Download 0104424 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T09:59:41
Download 3254cfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:45 CET (sv-comp)
Download 4c0337a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T19:36:12+01:00 Download e9ee94c
Download 202bbb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:21:43+01:00 Download d3e5e3f
Download ebac265 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:52:58+01:00 Download 8afd150
Download 60cb667 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T17:36:43+01:00 Download a16a409
Download da05ed8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:20:29+01:00 Download 6510a68
Download 450b210 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:44:10+01:00 Download 0104424
Download aab24a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T03:58:22+01:00 Download be27474
Download 4ebd375 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:45:29+01:00 Download e127fc8
Download 3374053 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:37:30+01:00 Download 3254cfb
Download 4342d4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:29:04+01:00 Download c41f47f
Download 09ac391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:45:32+01:00 Download 0dd46d4
Download 08f025f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:17:48+01:00 Download c23935c
Download cb6e4de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:14:43+01:00 Download 2cf1df9
Download de0b18d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:05:35+01:00 Download d1f023d
Download 0dd46d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T21:20:52+01:00

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

Trying to find witnesses for program (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 24 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 04c5ead Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T22:28:06+01:00
Download cbfce7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T05:33:54+01:00
Download 73eff0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T04:37Z
Download 131c4bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T06:12 CET (sv-comp)
Download e3266cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T17:56Z
Download 203b1a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T16:56:06.116027
Download c354865 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T09:06:01.006044
Download df78828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-12-02T20:19:40+01:00
Download d458fc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-01T00:18:26+01:00
Download b7d90f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T07:01:10+01:00 55f28dc
Download 8bdce75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:29:50+01:00 19b2dc7
Download e3f4336 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T02:58:35+01:00 b67e2a6
Download d11318a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T02:19:18+01:00 48e3f05
Download 36ad7ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:15:40+01:00 f0111ee
Download 74d5b11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T07:36:55+01:00 c6ad28a
Download 3cd70b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:38:01+01:00 5592365
Download 19b6d15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:13:53+01:00 7c838b7
Download bf2dbc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T07:00:18+01:00 21fdd2c
Download f09aaa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:03:58+01:00 1beef64
Download 7424e9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:02:48+01:00 c1eeab0
Download 0d1cd40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T18:57:30+01:00
Download 2f08aad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T18:21 CET (sv-comp)
Download 6f840ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T15:36Z
Download 25ae491 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 8 2017-12-01T02:46 CET (sv-comp)

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

Trying to find witnesses for program (edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5, sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/inv_square_int_true-unreach-call_true-termination.c, edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/edf09c27992d05d8e462d19e54c33ba82d90f4ee4a8b6d8f63933fed97aefbb5.json

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