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/ldv-regression/stateful_check_false-unreach-call_false-termination.i
programSHA 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
witnessName results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.stateful_check_false-unreach-call_false-termination.i.files/witness.graphml
witnessSHA 0cce2dd1a7159cbe5be5620276c1711898a30f559c875bd7c1bcab3e2d737ee4

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/0cce2dd1a7159cbe5be5620276c1711898a30f559c875bd7c1bcab3e2d737ee4.json

Key Value
architecture 32bit
creationtime 2017-11-30T23:18 CET (sv-comp)
producer 2LS
program-sha256 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
programfile ../../sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i
programhash 1225f82562543767c482452e9133e4a69d5dae70
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0cce2dd1a7159cbe5be5620276c1711898a30f559c875bd7c1bcab3e2d737ee4.graphml
witness-sha256 0cce2dd1a7159cbe5be5620276c1711898a30f559c875bd7c1bcab3e2d737ee4
witness-size 9233
witness-type violation_witness

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

Trying to find witnesses for program (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.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 (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.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 (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.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 (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.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 (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 22 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1e7eac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 3 2019-12-01 22:11:10
Download 9485724 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 13 2019-12-03T22:06 CET (comp)
Download 6d73d68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-11T21:58:29+01:00 Download dc78271
Download 17f23e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-11T21:43:46+01:00 Download 4175197
Download be46c77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-11T21:09:02+01:00 Download 1e7eac2
Download f93905d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T20:54:20+01:00 Download 1a20482
Download 3981322 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 130 2019-12-11T20:44:27+01:00 Download 1229218
Download dc7655f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-08T01:51:16+01:00 Download 058dc0c
Download 18186f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-08T00:26:02+01:00 Download d901158
Download 2f1ed96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-07T21:15:57+01:00 Download 0a75916
Download 91db1d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-04T02:58:17+01:00 Download 9485724
Download 28d4c51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-03T08:57:15+01:00 Download fb3b5c4
Download 59c2aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-03T08:10:33+01:00 Download a2c894c
Download a2c894c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 21 2019-11-30T13:34:22+01:00
Download 058dc0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 24 2019-12-07T21:07:16+01:00
Download dc78271 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 24 2019-12-01T00:30:32+01:00
Download ce8d36c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-08T00:06:06+01:00 Download 6499501
Download ea6849a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-05T20:20:14+01:00 Download 7658021
Download ece3e27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-05T19:34:11+01:00 Download 678d5c7
Download b12d9ba Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 1 2019-12-01 12:04:04
Download f88bf91 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 21 2019-11-30T12:01:03+01:00
Download b0eb35c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 21 2019-12-01T17:44:05+01:00

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

Trying to find witnesses for program (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 26 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c4763f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T12:41 CET (sv-comp)
Download b64c56d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 5 2018-12-07T21:39:20
Download 8b28bab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 24 2018-12-10T17:39:42+01:00
Download d0e5e2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 21 2018-12-07T13:20:21+01:00
Download 9669893 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-10T20:36:27+01:00 Download 8b28bab
Download 5994aaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-10T10:48:41+01:00 Download fa028b7
Download adec096 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-09T20:53:08+01:00 Download e1f0ebe
Download b56a32f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-09T20:38:58+01:00 Download 58d0cf0
Download 6b14042 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-09T20:23:20+01:00 Download 91f7f9c
Download fd3a268 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 430 2018-12-09T18:20:44+01:00 Download 363fe06
Download 6a65ffa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T23:44:03+01:00 Download c4763f8
Download 4b01c06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 46 2018-12-08T22:10:23+01:00 Download b64c56d
Download 6a7316a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T07:45:38+01:00 Download d0e5e2d
Download 7fb0b24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T05:03:20+01:00 Download 499b3f3
Download ee64a17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T04:36:53+01:00 Download fa028b7
Download 570355f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-06T10:19:21+01:00 Download 61d3bbe
Download 94cc15c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-06T09:49:11+01:00 Download c0dc24e
Download ea9678e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-06T09:09:34+01:00 Download cc88790
Download c0dc24e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T05:44:31+01:00
Download 4f747d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-07T09:20:32+01:00 Download b067243
Download bd61638 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:40:29+01:00 Download abe9bc0
Download 3accc8a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 21 2018-12-06T23:59:08+01:00
Download 504cad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:33:23+01:00
Download b90c2c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T10:18:45+01:00
Download 716f039 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T09:40:28+01:00
Download 0dd4d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T01:03:45+01:00

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

Trying to find witnesses for program (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 19 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9b76c74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 21 2017-12-03T04:31Z
Download c8562bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T09:30 CET (sv-comp)
Download b067243 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 5 2017-12-01T20:41 CET (sv-comp)
Download 49df642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 21 2017-12-02T05:15Z
Download 321c75c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T00:07:47.254772
Download aa88f22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T13:08:45.584878
Download 268d30f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-12-01T20:28 CET (sv-comp)
Download e1a0191 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-11-30T22:58 CET (sv-comp)
Download 828316d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 29 2017-12-03T01:06:14+01:00
Download 97451d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 21 2017-11-30T15:35:28+01:00
Download 7f2b860 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 29 2017-11-30T15:31:18+01:00
Download 7346899 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 18 2017-12-01T00:29:48+01:00
Download d15c9e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 21 2017-12-01T21:48:53+01:00
Download 9238361 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 17 2017-12-01T02:21 CET (sv-comp)
Download ae3edb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 21 2017-12-02T02:30Z
Download 0cce2dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 9 2017-11-30T23:18 CET (sv-comp)
Download cb7abd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 21 2017-12-01T18:17:46+01:00
Download cf4ed9a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 7 2017-12-03T11:15Z
Download da6d59b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 4 2017-12-01T12:51 CET (sv-comp)

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

Trying to find witnesses for program (73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814, sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json

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