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_2_true-unreach-call_false-termination.i
programSHA 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
witnessName results-validated/cpa-seq-validate-correctness-witnesses-cpa-seq.2018-12-06_0837.logfiles/sv-comp19_prop-reachsafety.while_infinite_loop_2_true-unreach-call_false-termination.i.files/witness.graphml
witnessSHA 0ef3af757bda012268ac5ef46cb1d7473b891e3824ad58f6f87bafdf9b4849e3

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:14:53+01:00
inputwitnesshash cd8405c53ac681760b9ed0d56e335598fde5cc85644259b64a92e1156e4667f1
producer CPAchecker 1.7-svn 29852
program-sha256 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
programfile ../../sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i
programhash 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0ef3af757bda012268ac5ef46cb1d7473b891e3824ad58f6f87bafdf9b4849e3.graphml
witness-sha256 0ef3af757bda012268ac5ef46cb1d7473b891e3824ad58f6f87bafdf9b4849e3
witness-size 4336
witness-type correctness_witness

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

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

Trying to find witnesses for program (7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2, sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i).

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

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

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

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

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

Found 18 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3e24bf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T13:10:11
Download 07ef2fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T09:02:30+01:00
Download c896d98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T19:57:54+01:00 Download 389a269
Download 7b57df2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:30:39+01:00 Download 99d288d
Download 8be39b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:19:55+01:00 Download dde4441
Download e63d0c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:08:37+01:00 Download 19d4667
Download 18023ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:58:50+01:00 Download 60faf12
Download 91a64b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:37:53+01:00 Download 3e24bf6
Download 63d6c74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T07:13:54+01:00 Download 07ef2fa
Download 7969da4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:17:34+01:00 Download 40d5a50
Download b58d6b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:07:50+01:00 Download 99d288d
Download 2d8f38f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:44:44+01:00 Download 85b2953
Download 7482516 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:28:21+01:00 Download ff8292e
Download 0ef3af7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:14:53+01:00 Download cd8405c
Download b8b40a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:00:24+01:00 Download e9cae65
Download cd8405c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T13:46:08+01:00
Download 281a4a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T20:42:18+01:00
Download 32763df Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T21:23:54+01:00

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

Trying to find witnesses for program (7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2, sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i).

Found 23 witnesses for program sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i, 7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 85b2953 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:16 CET (sv-comp)
Download c917ae5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-02T21:14Z
Download 81943aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T10:55Z
Download c5b08f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T18:46:17.690061
Download bb84d08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T16:39 CET (sv-comp)
Download 764c3ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 5 2017-12-02T19:32:30+01:00
Download 73b9baa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T03:58:42+01:00
Download 53287bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T01:37:41+01:00 0ae96d2
Download 0d6e0f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T14:38:39+01:00 2ee846c
Download 979c6a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T07:53:43+01:00 d850489
Download 464c77f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:15:14+01:00 7d83451
Download 02fd390 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:56+01:00 978185e
Download 0303778 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:04:41+01:00 7b6cff4
Download f616cea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:11:03+01:00 d84d67e
Download aec66da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T03:54:14+01:00
Download 8f0b822 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 6 2017-11-30T12:22:30+01:00
Download e99aad1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T23:42:26+01:00
Download a93b209 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-01T19:20:53+01:00
Download 9fa018c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T18:43Z
Download d3aa5dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 8 2017-12-01T03:10 CET (sv-comp)
Download 7b2d11e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T15:59:41+01:00
Download 48ef298 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 5 2017-12-03T11:13Z
Download e3435d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 5 2017-12-01T15:16 CET (sv-comp)

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

Trying to find witnesses for program (7a375449cd377c6579da2bbc04cf21b60d21a48b2c49fb299e3a13735e9a17c2, sv-benchmarks/c/loops/while_infinite_loop_2_true-unreach-call_false-termination.i).

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

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