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/square_6_true-unreach-call_true-termination.i
programSHA 6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.square_6_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA aff5b86ca2562384ee7187c73c45acdfca03586a877a5963369ccab128b7ec88

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T10:02 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i
programhash 20673ed10b5a05371c8641d8d8a54d9346cb443e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/aff5b86ca2562384ee7187c73c45acdfca03586a877a5963369ccab128b7ec88.graphml
witness-sha256 aff5b86ca2562384ee7187c73c45acdfca03586a877a5963369ccab128b7ec88
witness-size 4715
witness-type correctness_witness

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

Trying to find witnesses for program (6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3, sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i).

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

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

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

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

Found 17 witnesses for program sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i, 6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 82b761e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:43 CET (comp)
Download d141d3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:16:54+01:00 Download acb5a5c
Download 0388367 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:13:00+01:00 Download ee343a3
Download 6d2fc71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:03:03+01:00 Download 0f0d4f5
Download 3460174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:36:27+01:00 Download 2a56f9a
Download ebf22c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:47:54+01:00 Download 797edfc
Download 2e00dee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:42:42+01:00 Download 1c0c1d4
Download 426e6ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:41:10+01:00 Download 25e2777
Download 4647ec7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:13:00+01:00 Download 74cda2f
Download a433ee2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:02:51+01:00 Download 54e39c0
Download 6102907 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:56+01:00 Download 82b761e
Download 90e2fb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T17:23:02+01:00 Download 128897a
Download 128897a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T13:56:36+01:00
Download 2a56f9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T14:53:49+01:00
Download acb5a5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T03:47:07+01:00
Download 797edfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:36:38Z
Download edbaa53 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:57 CET (comp)

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

Trying to find witnesses for program (6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3, sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i).

Found 14 witnesses for program sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i, 6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0257498 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T22:42 CET (sv-comp)
Download 8e01fac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 4 2018-12-10T18:04:28+01:00
Download 230e8e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T10:20:19+01:00
Download 2317913 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:06:57+01:00 Download 8e01fac
Download c8e9fe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T06:09:41+01:00 Download 230e8e8
Download b666584 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T03:05:52+01:00 Download 437c9e0
Download 7d6a2d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:42:03+01:00 Download 0257498
Download a08ad37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:32:34+01:00 Download 1aa82ab
Download 618bb9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:06:38+01:00 Download 342676d
Download 0e86c2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:26:16+01:00 Download a30ac23
Download a882e90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:18:37+01:00 Download aff5b86
Download 9ec4275 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:56:02+01:00 Download c0d1559
Download 342676d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T23:42:40+01:00
Download 89c3cc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T00:57 CET (sv-comp)

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

Trying to find witnesses for program (6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3, sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i).

Found 22 witnesses for program sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i, 6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 83dcc77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T18:20:46+01:00
Download 6097428 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T22:16:07+01:00
Download 97a761e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:01 CET (sv-comp)
Download 17c3063 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T03:04Z
Download d58e599 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:23:17.084834
Download e9fe1bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:18:50.793897
Download 50e00ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T19:05:39.709987
Download 5d55250 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T12:58:50.057966
Download e45989b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T06:55:58+01:00 51f024b
Download ba3028f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:35:14+01:00 ec7a287
Download a933414 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T09:05:38+01:00 a123c12
Download f10d269 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:13:44+01:00 eebec7a
Download ef256fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:33:41+01:00 06689c2
Download 5abf1a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T07:20:20+01:00 91de0f1
Download d4c5ae7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:27:14+01:00 8c61ae6
Download dff5a28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:28:43+01:00 792144e
Download 1c8a1b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T12:10:59+01:00
Download 00df69b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T17:59 CET (sv-comp)
Download 84c2647 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T00:21Z
Download 64fca6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-11-30T15:19 CET (sv-comp)
Download 48c87fe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T13:50 CET (sv-comp)
Download 9a9a93d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T16:26 CET (sv-comp)

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

Trying to find witnesses for program (6d5d78ed49d1fcde932863bc3cc65bedd0b892488c4337c323747111ab0fb3e3, sv-benchmarks/c/floats-cdfpl/square_6_true-unreach-call_true-termination.i).

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

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