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/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c
programSHA 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.Problem01_label35_false-unreach-call_false-termination.c.files/witness.graphml
witnessSHA cde0732e893f3aa4aee4043f33a572e13b828e4892a8754e6212a36d2178012b

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T14:56:20.122030
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c
programhash e1627e38bed35af1698e9f3e6e9827d6a9566f03
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/cde0732e893f3aa4aee4043f33a572e13b828e4892a8754e6212a36d2178012b.graphml
witness-sha256 cde0732e893f3aa4aee4043f33a572e13b828e4892a8754e6212a36d2178012b
witness-size 4607
witness-type violation_witness

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

Trying to find witnesses for program (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.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 (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.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 (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.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 (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.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 (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 42e167c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 14:15:23
Download b0202c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 53 2019-12-03T22:44 CET (comp)
Download 30a3a5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 156 2019-12-11T21:43:41+01:00 Download cac075b
Download 4ecf1dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 155 2019-12-11T21:09:22+01:00 Download 42e167c
Download 57b7015 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 156 2019-12-11T20:55:12+01:00 Download 642ab6c
Download 7b6d108 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 156 2019-12-11T20:44:36+01:00 Download cd5dcc8
Download 3d31f88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 157 2019-12-08T01:51:29+01:00 Download 88e8579
Download c200ee1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 197 2019-12-04T02:58:24+01:00 Download b0202c4
Download 172334a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 156 2019-12-03T08:09:52+01:00 Download 2b8ed64
Download 2b8ed64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 154 2019-11-29T22:54:37+01:00
Download cac075b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 155 2019-12-01T09:04:51+01:00
Download 276ef6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T21:42:38+01:00 Download 8bf477b
Download 48082f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-08T00:27:18+01:00 Download 6ede73d
Download b315091 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T21:17:17+01:00 Download e148213
Download 23758ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T20:22:49+01:00 Download 886dea2
Download 1f42820 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T19:35:32+01:00 Download c237975
Download a8a2e72 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 339 2019-11-30T05:30:33+01:00
Download 0cf2eb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 339 2019-12-01T00:40:59+01:00

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

Trying to find witnesses for program (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d565249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T08:31 CET (sv-comp)
Download 1402988 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 8 2018-12-08T12:00:45
Download 1d0f81f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 62 2018-12-06T21:18 CET (sv-comp)
Download ef9b6ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 155 2018-12-06T20:04:24+01:00
Download 19d9d77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 157 2018-12-10T20:38:09+01:00 Download 5319bf5
Download c6fc116 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 156 2018-12-09T18:20:23+01:00 Download d06059c
Download 6984681 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 157 2018-12-08T23:43:08+01:00 Download d565249
Download 1763d0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 156 2018-12-08T22:10:48+01:00 Download 1402988
Download 49ae180 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 156 2018-12-08T08:36:05+01:00 Download ef9b6ab
Download 865ca0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 156 2018-12-08T04:52:38+01:00 Download cde0732
Download 6f7944e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 197 2018-12-07T17:44:32+01:00 Download 1d0f81f
Download f322278 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 156 2018-12-06T10:17:26+01:00 Download 55e20c6
Download a408026 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 156 2018-12-06T09:48:24+01:00 Download 14fae7c
Download e6c48af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 197 2018-12-06T09:11:55+01:00 Download 7b09083
Download 14fae7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 154 2018-12-06T06:02:17+01:00
Download 3db14b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:53:44+01:00 Download be47930
Download 5b4397c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:38:13+01:00 Download 88197c6
Download a683395 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:20:15+01:00 Download df2698f
Download 8302ab8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:42:00+01:00 Download 4c75a07
Download dab6596 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 339 2018-12-07T09:02:55+01:00
Download 26ee630 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-08T08:20:05+01:00
Download 4f2a89b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T09:49:07+01:00
Download d7da061 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 327 2018-12-05T10:46:04+01:00

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

Trying to find witnesses for program (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fba8b7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 4 2017-12-02T23:49 CET (sv-comp)
Download a348054 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:04 CET (sv-comp)
Download 3293414 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 134 2017-12-02T03:23Z
Download 896f2c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T21:22:10.508072
Download 718ce07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T07:53:47.697815
Download 008fc67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 13 2017-12-01T20:13 CET (sv-comp)
Download 0cd7560 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 13 2017-12-01T02:40 CET (sv-comp)
Download 076e12c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 91 2017-12-01T00:48:56+01:00
Download 05cf281 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 224 2017-11-30T19:24:56+01:00
Download 61c9550 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 87 2017-11-30T16:49:28+01:00
Download b4bc767 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 139 2017-12-02T00:44:01+01:00
Download 65fa871 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 67 2017-11-30T22:47 CET (sv-comp)
Download 2c376c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 134 2017-12-02T01:34Z
Download a30743e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 68 2017-11-30T22:06 CET (sv-comp)
Download b9e4807 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 31 2017-12-01T15:41 CET (sv-comp)

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

Trying to find witnesses for program (4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe, sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c, 4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4033184f1bf11db44f676cb06dde4a0ba53e41fe347aa143123e74ed0723dabe.json

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