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/sum01_false-unreach-call_true-termination.i
programSHA daea4f265492688926b0240bb8b10d0ae4a79ee7f95347220e899a623a02ea88
witnessName results-validated/cpa-seq-validate-violation-witnesses-2ls.2018-12-06_0936.logfiles/sv-comp19_prop-reachsafety.sum01_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 39fcd41a991422d56cf9d0920155c72bffeef961f5bd4f42ff292985b81e3dec

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:41:11+01:00
inputwitnesshash e8c4a8f8581a66282104448ca13e8792b3074f27d2c917b89becc31dfa737243
producer CPAchecker 1.7-svn 29852
program-sha256 daea4f265492688926b0240bb8b10d0ae4a79ee7f95347220e899a623a02ea88
programfile ../../sv-benchmarks/c/loops/sum01_false-unreach-call_true-termination.i
programhash daea4f265492688926b0240bb8b10d0ae4a79ee7f95347220e899a623a02ea88
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/39fcd41a991422d56cf9d0920155c72bffeef961f5bd4f42ff292985b81e3dec.graphml
witness-sha256 39fcd41a991422d56cf9d0920155c72bffeef961f5bd4f42ff292985b81e3dec
witness-size 6827
witness-type correctness_witness

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

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

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

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

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

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

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

Found 18 witnesses for program sv-benchmarks/c/loops/sum01_false-unreach-call_true-termination.i, daea4f265492688926b0240bb8b10d0ae4a79ee7f95347220e899a623a02ea88
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/daea4f265492688926b0240bb8b10d0ae4a79ee7f95347220e899a623a02ea88.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6bc5fa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 05:42:52
Download c40c9b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 11 2019-12-03T22:43 CET (comp)
Download ad29b55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness GACAL 17 2019-12-07T22:44 CET (comp)
Download 1724297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-11T21:57:11+01:00 Download 52fa465
Download 960f1a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 25 2019-12-11T21:48:11+01:00 Download b78901b
Download 7ac28bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-11T21:09:20+01:00 Download 6bc5fa6
Download 3b8eb8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 25 2019-12-11T20:54:22+01:00 Download d22d2bc
Download 8f4a5fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 66 2019-12-11T20:45:01+01:00 Download e43af03
Download b75887c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-08T01:51:14+01:00 Download 63f7ceb
Download 3cb62d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 25 2019-12-08T00:27:17+01:00 Download 8fc041c
Download d148cbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 25 2019-12-07T21:18:22+01:00 Download b6107e6
Download a22a792 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 18 2019-12-04T02:58:25+01:00 Download c40c9b8
Download dddb052 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 24 2019-12-03T08:09:55+01:00 Download 152e510
Download 152e510 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 25 2019-11-30T03:23:14+01:00
Download 63f7ceb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 25 2019-12-07T22:23:31+01:00
Download 52fa465 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 24 2019-12-01T01:32:13+01:00
Download a935a36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T20:21:39+01:00 Download 80bd4b2
Download 42b32b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T19:34:16+01:00 Download 4ac45f8

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c25db3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T13:35 CET (sv-comp)
Download 170c190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 8 2018-12-07T23:32:47
Download f78319a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 23 2018-12-10T18:20:24+01:00
Download 31f07bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 25 2018-12-07T02:56:46+01:00
Download 692f1fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-10T20:38:26+01:00 Download f78319a
Download b573cab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-09T20:26:12+01:00 Download 0963d58
Download 023a2c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-09T18:20:00+01:00 Download cd51811
Download fe8502a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-08T23:43:50+01:00 Download c25db3f
Download 9e05b0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-08T22:08:02+01:00 Download 170c190
Download 38bd5ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T08:24:02+01:00 Download 31f07bb
Download 4cae86b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-08T05:04:58+01:00 Download d144693
Download 477d0b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-07T18:15:29+01:00 Download 7cb22ee
Download b1a0c17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-06T10:18:04+01:00 Download a71e451
Download 95501d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-06T09:48:43+01:00 Download 48c1fb3
Download 9b0b0e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-06T09:17:07+01:00 Download 39d511d
Download 48c1fb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-05T15:54:14+01:00
Download f2f3451 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T21:23:35+01:00 Download a0908dc
Download 4f0c65c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:08+01:00 Download b43ea2b
Download dd15742 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:38:52+01:00 Download e9fea56
Download 39fcd41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:41:11+01:00 Download e8c4a8f
Download 0953b60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:11:17+01:00 Download 5e5de7d

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b45f71e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 6 2017-12-01T22:04 CET (sv-comp)
Download e0de7a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 893 2017-12-03T03:53 CET (sv-comp)
Download 0a0b478 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 15 2017-12-02T19:51Z
Download a12a4f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-01T23:03 CET (sv-comp)
Download bec8a28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 15 2017-12-02T17:10Z
Download fa9865b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T23:21:31.130756
Download 5abce30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:46:19.660929
Download 9161ad5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 8 2017-12-01T21:41 CET (sv-comp)
Download 8f98c84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 8 2017-12-01T02:16 CET (sv-comp)
Download 006b416 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 21 2017-12-02T20:34:37+01:00
Download 90af245 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 23 2017-11-30T18:27:25+01:00
Download 2572aea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 27 2017-11-30T20:20:58+01:00
Download 4106363 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 18 2017-11-30T21:23:09+01:00
Download 602bf52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 18 2017-12-02T06:47:18+01:00
Download b35df72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 12 2017-12-01T00:36 CET (sv-comp)
Download 332fcd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 15 2017-12-02T13:25Z
Download 3208e07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 11 2017-11-30T20:28 CET (sv-comp)
Download a211741 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T20:28 CET (sv-comp)
Download cdfe26e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:37:22+01:00 f9529e1

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

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

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

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