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/loops/invert_string_true-unreach-call_true-termination.i
programSHA 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
witnessName results-validated/cpa-seq-validate-correctness-witnesses-cbmc.2018-12-06_0735.logfiles/sv-comp19_prop-reachsafety.invert_string_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA f0b87852f0432b175cb15419446e078e3efb3b671d8bd196478a6b690dfc3462

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T08:17:22+01:00
inputwitnesshash 0e0a3a59979a845b4968881ba8661585bfbe31988829784437f0b46381666e91
producer CPAchecker 1.7-svn 29852
program-sha256 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
programfile ../../sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i
programhash 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/f0b87852f0432b175cb15419446e078e3efb3b671d8bd196478a6b690dfc3462.graphml
witness-sha256 f0b87852f0432b175cb15419446e078e3efb3b671d8bd196478a6b690dfc3462
witness-size 7243
witness-type correctness_witness

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

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

Trying to find witnesses for program (7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861, sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i).

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.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 (7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861, sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i).

Found 24 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a177881 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T16:30 CET (sv-comp)
Download d3f57ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:19:30
Download 543dd9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:15 CET (sv-comp)
Download 035260f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 8 2018-12-10T17:49:36+01:00
Download 1fa23dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-07T10:34:37+01:00
Download 650afe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:09:55+01:00 Download 035260f
Download 6e8d1ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T21:06:38+01:00 Download 7ebf521
Download 97fb492 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:06:47+01:00 Download d1cdf05
Download c6b05b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T19:49:26+01:00 Download fa267e9
Download b8733e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:15:41+01:00 Download a177881
Download 5e282aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T21:46:37+01:00 Download d3f57ba
Download 3f7b933 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T06:00:58+01:00 Download 1fa23dd
Download 98b56ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T04:03:25+01:00 Download 9422bfe
Download 9980eed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T02:33:57+01:00 Download 19e7e05
Download 721e8d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T17:45:19+01:00 Download 6797ee6
Download 5a80c97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T16:39:38+01:00 Download 543dd9e
Download 6446b7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:29:12+01:00 Download 8b38a9c
Download e69eed7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T08:56:04+01:00 Download af9af57
Download f0b8785 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T08:17:22+01:00 Download 0e0a3a5
Download 5060c36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:53:26+01:00 Download bb22cdf
Download e6aff01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:13:23+01:00 Download 63c776c
Download af9af57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-05T22:33:24+01:00
Download e3731cb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T06:39 CET (sv-comp)
Download 05e834c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T04:00 CET (sv-comp)

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

Trying to find witnesses for program (7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861, sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i).

Found 35 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ef04229 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 29 2017-12-01T03:47:17+01:00
Download 96d6a22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 15 2017-12-01T02:30:39+01:00
Download 6797ee6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:11 CET (sv-comp)
Download 1688888 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 11 2017-12-02T23:16Z
Download 29ad765 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T13:20 CET (sv-comp)
Download 32937d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T21:22 CET (sv-comp)
Download 994c27e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 19 2017-12-02T12:50Z
Download 7cdfc15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:24:42.324181
Download a23b835 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:11:19.725351
Download 23f51e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T14:39:22.572148
Download b71de2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:05:26.133934
Download efa701c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T16:32 CET (sv-comp)
Download 84361d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 9 2017-12-02T21:36:38+01:00
Download a959d3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T05:42:53+01:00
Download 086b7d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T07:02:54+01:00 b773eb7
Download 4f56c75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T04:23:47+01:00 d0b9598
Download 28398de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T01:33:29+01:00 5df9d7c
Download 6889fcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T00:48:04+01:00 816b789
Download 46a6f56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T20:47:21+01:00 0167bbd
Download 23e9626 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T15:13:56+01:00 eaad0e9
Download 374eb47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T08:19:18+01:00 1a15f48
Download d14b1c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T00:06:47+01:00 c719998
Download ce9e42a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:26:23+01:00 1955fc1
Download 054c69d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:08:40+01:00 f42677e
Download 88ec782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:12:45+01:00 ffadc85
Download 1ab7b8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:41:21+01:00 e1e8635
Download feba057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:17:24+01:00 31c7807
Download 6307242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T05:01:18+01:00 09de94b
Download 902b848 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T03:28:02+01:00
Download 6e4eb6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 8 2017-12-02T09:44:56+01:00
Download e407130 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 22 2017-11-30T15:46 CET (sv-comp)
Download c8e101f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 11 2017-12-02T09:50Z
Download 60343c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 41 2017-11-30T21:51 CET (sv-comp)
Download 56f957b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 21 2017-12-01T16:10 CET (sv-comp)
Download 0ad01b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T11:50 CET (sv-comp)

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

Trying to find witnesses for program (7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861, sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_true-unreach-call_true-termination.i, 7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7d1e1085960ce45c0ce267f697714b70bddb591dd05a4bcb4b118a4ce9db6861.json

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