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/while_infinite_loop_4_false-unreach-call_true-termination.i
programSHA 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
witnessName results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.while_infinite_loop_4_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 3ff78e0fb6c4802bc7b4bb926e1c65d1f719abb1bd2171594d0a33bec9df5a50

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/3ff78e0fb6c4802bc7b4bb926e1c65d1f719abb1bd2171594d0a33bec9df5a50.json

Key Value
architecture 32bit
creationtime 2017-12-01T14:29:00.575158
producer ESBMC 4.6.0 incr
program-sha256 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
programfile ../../sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i
programhash 66fc6b12b7cd24de7373fe06aeeb5aec1e7e0e8b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3ff78e0fb6c4802bc7b4bb926e1c65d1f719abb1bd2171594d0a33bec9df5a50.graphml
witness-sha256 3ff78e0fb6c4802bc7b4bb926e1c65d1f719abb1bd2171594d0a33bec9df5a50
witness-size 3616
witness-type violation_witness

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

Trying to find witnesses for program (454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b, sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i).

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

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

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

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

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

Found 27 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4ac0779 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T05:46 CET (sv-comp)
Download 9baa140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T08:33:40
Download 381d47b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2018-12-07T01:04 CET (sv-comp)
Download 67dd730 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 5 2018-12-10T17:10:50+01:00
Download d278768 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T19:06:58+01:00
Download 3758082 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:34:56+01:00 Download 67dd730
Download 28cdbb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:48:58+01:00 Download 56501c9
Download 70dc314 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:26+01:00 Download 1e9b592
Download a960ec1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:39:16+01:00 Download 57583b8
Download dcaeb16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:23:13+01:00 Download 0b0f86c
Download fafb5ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:58:56+01:00 Download 8b2e561
Download 126a92e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:42:12+01:00 Download 4ac0779
Download 3a9ccb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:09:00+01:00 Download 9baa140
Download d84a756 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T07:47:29+01:00 Download d278768
Download eb6f976 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:06:08+01:00 Download d26102a
Download 95e5081 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:37:04+01:00 Download 56501c9
Download 82b3caf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T18:47:04+01:00 Download b750eb7
Download fb0c451 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:43:20+01:00 Download 381d47b
Download 42578af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:10:18+01:00 Download da84b8b
Download 85caea9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:13:38+01:00 Download b4fae12
Download bc49067 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:18+01:00 Download c077626
Download 4da9b15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:06:06+01:00 Download cd11533
Download 8f8417e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:00:15+01:00 Download 4729a5c
Download c077626 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:10:22+01:00
Download 0a3c977 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:40:46+01:00 Download 2d427ee
Download 89dfd15 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T06:47 CET (sv-comp)
Download c2d61f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T01:20 CET (sv-comp)

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

Trying to find witnesses for program (454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b, sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i).

Found 21 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i, 454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 09ad22b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:05 CET (sv-comp)
Download 44746a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 6 2017-12-02T17:33Z
Download 259ee94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T17:46 CET (sv-comp)
Download 1e1f0f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T21:45 CET (sv-comp)
Download 356b8ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 6 2017-12-02T20:36Z
Download 1321aaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T01:12:34.198404
Download 3ff78e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T14:29:00.575158
Download 26423e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T19:51 CET (sv-comp)
Download 4aaad7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T21:14 CET (sv-comp)
Download 556071d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 6 2017-12-03T02:15:44+01:00
Download b160316 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T19:17:54+01:00
Download 197561b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 7 2017-11-30T16:00:08+01:00
Download 5ff78c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T20:41:17+01:00
Download cb3d7be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T22:31:39+01:00
Download e44419c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-12-01T01:46 CET (sv-comp)
Download 38cdf25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T08:23Z
Download 2d427ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T13:52 CET (sv-comp)
Download d7529da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:53:09.233452
Download a00217f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:56:09.158634
Download b8794d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 6 2017-12-01T11:53 CET (sv-comp)
Download 2f09956 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T13:46 CET (sv-comp)

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

Trying to find witnesses for program (454b4af8a1b369cb3b509d067b2e3943e8e7e79e43bf459c28bb55cd1e6de22b, sv-benchmarks/c/loops/while_infinite_loop_4_false-unreach-call_true-termination.i).

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

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