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_label47_false-unreach-call_false-termination.c
programSHA e8149a6178cde7de162cd9e897c551aeb605d4c24297c55cf44904326b78f2a8
witnessName results-validated/cpa-seq-validate-violation-witnesses-veriabs.2018-12-10_2034.logfiles/sv-comp19_prop-reachsafety.Problem01_label47_false-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 17bdb3cfe746391c6b2099458193c0f1ae1c1ad2294a2ad7c28e2361b43d5fb7

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T20:37:53+01:00
inputwitnesshash c3f55b7fa6fab4bbc98cc08b465e9647fb22d956576be4a4195514a8b4473c05
producer CPAchecker 1.7-svn 29852
program-sha256 e8149a6178cde7de162cd9e897c551aeb605d4c24297c55cf44904326b78f2a8
programfile ../../sv-benchmarks/c/eca-rers2012/Problem01_label47_false-unreach-call_false-termination.c
programhash e8149a6178cde7de162cd9e897c551aeb605d4c24297c55cf44904326b78f2a8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/17bdb3cfe746391c6b2099458193c0f1ae1c1ad2294a2ad7c28e2361b43d5fb7.graphml
witness-sha256 17bdb3cfe746391c6b2099458193c0f1ae1c1ad2294a2ad7c28e2361b43d5fb7
witness-size 201092
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0fcee9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 15:12:58
Download 113fb49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 70 2019-12-03T23:22 CET (comp)
Download a8f3d7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 199 2019-12-11T21:55:20+01:00 Download fb33fea
Download 6450fcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 199 2019-12-11T21:09:45+01:00 Download 0fcee9a
Download 7d7d0c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 200 2019-12-11T20:54:52+01:00 Download 51202fe
Download c1fb3a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 200 2019-12-11T20:44:29+01:00 Download a2a57d1
Download 0a4d75f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 201 2019-12-08T01:51:38+01:00 Download 721de81
Download cb6f8e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 249 2019-12-04T02:58:22+01:00 Download 113fb49
Download 8ce98cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 199 2019-12-03T08:09:33+01:00 Download 2983a20
Download 2983a20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 197 2019-11-30T09:35:43+01:00
Download fb33fea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 198 2019-12-01T13:58:04+01:00
Download 452025f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T21:40:22+01:00 Download ef96c30
Download bb753e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-08T00:27:02+01:00 Download d944bd5
Download 7292753 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T21:16:06+01:00 Download 29fcd8e
Download 451e61e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T20:22:42+01:00 Download a420ba3
Download 0922fcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T19:35:10+01:00 Download a64652c
Download 0496979 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 339 2019-11-30T12:21:32+01:00
Download 6519463 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 339 2019-12-01T02:25:49+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 348aefd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T06:38 CET (sv-comp)
Download 0f7b9b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 11 2018-12-08T00:51:15
Download 4458c61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 81 2018-12-07T01:38 CET (sv-comp)
Download e5bbe30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 198 2018-12-07T14:48:02+01:00
Download 17bdb3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 201 2018-12-10T20:37:53+01:00 Download c3f55b7
Download 82958af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 200 2018-12-09T18:21:33+01:00 Download df73f91
Download 9d89d1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 203 2018-12-08T23:43:50+01:00 Download 348aefd
Download 7859a39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 200 2018-12-08T22:07:53+01:00 Download 0f7b9b0
Download 98cba9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 199 2018-12-08T08:29:24+01:00 Download e5bbe30
Download 353fa62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 200 2018-12-08T05:04:21+01:00 Download 2b1ff80
Download 6798bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 249 2018-12-07T17:44:46+01:00 Download 4458c61
Download 95585ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 200 2018-12-06T10:12:21+01:00 Download 5fc296b
Download 808e326 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 199 2018-12-06T09:48:16+01:00 Download e3cccf4
Download 1361ec3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 250 2018-12-06T09:08:34+01:00 Download 56b5977
Download e3cccf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 197 2018-12-06T01:42:38+01:00
Download 2bd9813 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:53:45+01:00 Download c61510c
Download 0251460 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:38:18+01:00 Download 3145927
Download a73dce2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:26:36+01:00 Download c5c168f
Download c1dd3c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:41:39+01:00 Download 8a3ded9
Download 590c611 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 339 2018-12-07T07:51:12+01:00
Download 5d7c8fb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-08T08:37:19+01:00
Download 0120a6f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T09:48:59+01:00
Download 26fe969 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 327 2018-12-06T06:43:03+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8d4afed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 4 2017-12-03T03:29 CET (sv-comp)
Download c2185e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-01T22:54 CET (sv-comp)
Download 57c21f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 176 2017-12-02T02:11Z
Download 71f91d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T21:43:43.977627
Download 58a812c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T12:06:41.130942
Download ff30f60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 16 2017-12-01T19:48 CET (sv-comp)
Download 879a32a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 16 2017-11-30T21:36 CET (sv-comp)
Download ebfb663 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 115 2017-11-30T21:32:51+01:00
Download 3e3cf5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 288 2017-11-30T11:23:45+01:00
Download 98dbe96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 109 2017-11-30T12:04:06+01:00
Download a76e3ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 173 2017-12-02T04:31:19+01:00
Download df423e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 123 2017-11-30T18:33 CET (sv-comp)
Download bfe6f60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 176 2017-12-02T14:53Z
Download 0436c96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 90 2017-11-30T15:55 CET (sv-comp)
Download 183edcf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 31 2017-12-01T12:33 CET (sv-comp)

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

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

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

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