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/nec40_true-unreach-call_true-termination.i
programSHA fa7ac6e58c76955913b988ad9887f9146c35e7a82f7673a80307599db3302b51
witnessName results-validated/cpa-seq-validate-correctness-witnesses-cpa-seq.2018-12-06_0837.logfiles/sv-comp19_prop-reachsafety.nec40_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 0a000ce2a41e8fd0969361b142cf06261336f0a42bb67f5e1362afd8d0ef03f4

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T08:52:14+01:00
inputwitnesshash 32a8642e13e7de2de730be9803ae321e7971260549ec09e546feb3e06311ca7f
producer CPAchecker 1.7-svn 29852
program-sha256 fa7ac6e58c76955913b988ad9887f9146c35e7a82f7673a80307599db3302b51
programfile ../../sv-benchmarks/c/loops/nec40_true-unreach-call_true-termination.i
programhash fa7ac6e58c76955913b988ad9887f9146c35e7a82f7673a80307599db3302b51
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0a000ce2a41e8fd0969361b142cf06261336f0a42bb67f5e1362afd8d0ef03f4.graphml
witness-sha256 0a000ce2a41e8fd0969361b142cf06261336f0a42bb67f5e1362afd8d0ef03f4
witness-size 6456
witness-type correctness_witness

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

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

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

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

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

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

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

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

Found 21 witnesses for program sv-benchmarks/c/loops/nec40_true-unreach-call_true-termination.i, fa7ac6e58c76955913b988ad9887f9146c35e7a82f7673a80307599db3302b51
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fa7ac6e58c76955913b988ad9887f9146c35e7a82f7673a80307599db3302b51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ad97c2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T20:34 CET (sv-comp)
Download 9dfef79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T03:54:50
Download c271fc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T15:31 CET (sv-comp)
Download 507b9e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-08T01:47:06+01:00
Download 158813e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:17:59+01:00 Download cd01327
Download 7430d29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:22:31+01:00 Download f06334f
Download 7fdcc08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T19:59:06+01:00 Download 53a2060
Download cc99276 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:21:55+01:00 Download ad97c2e
Download da42437 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:41:39+01:00 Download 9dfef79
Download c0183df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T06:23:41+01:00 Download 507b9e6
Download 86333fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:51:01+01:00 Download 9ea8e85
Download b33cc28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T02:27:56+01:00 Download 676ec7b
Download e663b65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:44:51+01:00 Download b8028c6
Download be57bd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:38:49+01:00 Download c271fc3
Download 7b6a0d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:17+01:00 Download 36dc22e
Download 0a000ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:52:14+01:00 Download 32a8642
Download c1745e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:44:14+01:00 Download 1420a59
Download e743afa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:24:37+01:00 Download 72a5910
Download 32a8642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-05T20:58:20+01:00
Download d0b2a63 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:43 CET (sv-comp)
Download affc488 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:16 CET (sv-comp)

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

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

Found 37 witnesses for program sv-benchmarks/c/loops/nec40_true-unreach-call_true-termination.i, fa7ac6e58c76955913b988ad9887f9146c35e7a82f7673a80307599db3302b51
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fa7ac6e58c76955913b988ad9887f9146c35e7a82f7673a80307599db3302b51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b8028c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:35 CET (sv-comp)
Download ebb5437 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 7 2017-12-02T18:17Z
Download ddb7543 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T17:41 CET (sv-comp)
Download 6619b17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T20:15 CET (sv-comp)
Download bfae714 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 7 2017-12-02T11:44Z
Download 5cc7f09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:49:24.650911
Download 5934171 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:39:37.978751
Download 8e7d3a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T22:37:25.528266
Download 1b80895 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T20:49:32.610095
Download 4e25f62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T21:36 CET (sv-comp)
Download 784f74c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-02T19:57:05+01:00
Download eb8d18c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T02:01:44+01:00
Download 6c9ab5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T07:05:46+01:00 8e2b538
Download 918413a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:10:29+01:00 67f6568
Download e7eb55b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T02:20:24+01:00 c1fe0bd
Download 30ee734 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T00:24:01+01:00 2af76b2
Download 37681c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:34:09+01:00 e53fddf
Download 5143401 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T15:18:22+01:00 1d16feb
Download 81c41ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T07:08:16+01:00 b02268b
Download 8806074 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T00:04:28+01:00 a4df2a2
Download 717c31c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:26:00+01:00 31cd5cd
Download 5036f39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:09:32+01:00 334c338
Download 554adb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:12:55+01:00 d9a594e
Download a8c4e02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:25:38+01:00 573595c
Download ccd58f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:23:55+01:00 cddcd80
Download 5b7930c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:11:30+01:00 129c8fd
Download 1550ab1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:27:07+01:00 4b4f920
Download 0723a76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T04:48:08+01:00 d6e6585
Download c18c475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T14:05:16+01:00
Download 14dfb93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T17:35:27+01:00
Download df66e07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T13:41:34+01:00
Download df14865 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-01T20:30:21+01:00
Download ab7b8a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 6 2017-12-01T01:07 CET (sv-comp)
Download b444afd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 7 2017-12-02T00:24Z
Download 12ed1ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 9 2017-11-30T14:50 CET (sv-comp)
Download 34898b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T19:14 CET (sv-comp)
Download 0592392 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T17:18 CET (sv-comp)

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

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

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

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