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/float-benchs/zonotope_tight_true-unreach-call_true-termination.c
programSHA 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
witnessName results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.zonotope_tight_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 15aae91bfb3df709a6c97e50f1aeacfb4884b34f6f2cbd60d6fdbf65d21e5adf

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/15aae91bfb3df709a6c97e50f1aeacfb4884b34f6f2cbd60d6fdbf65d21e5adf.json

Key Value
architecture 32bit
creationtime 2017-12-02T03:33:19.317965
producer ESBMC 4.6.0 kind
program-sha256 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
programfile ../../sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c
programhash 7de8352890f1d55270cdee8daa00c3bfaf4226ea
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/15aae91bfb3df709a6c97e50f1aeacfb4884b34f6f2cbd60d6fdbf65d21e5adf.graphml
witness-sha256 15aae91bfb3df709a6c97e50f1aeacfb4884b34f6f2cbd60d6fdbf65d21e5adf
witness-size 3418
witness-type correctness_witness

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

Trying to find witnesses for program (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.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 (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.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 (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.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 (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.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 (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7e78bbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:30 CET (comp)
Download 47c8fd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:27:13+01:00 Download 36dfc9f
Download de59c53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:18:15+01:00 Download 9cde24b
Download 411f2a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:48+01:00 Download 03bf3e4
Download c4f951e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:55:05+01:00 Download 9a49a8b
Download 4b46b95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:47:15+01:00 Download 044a3eb
Download 577beaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:44:18+01:00 Download 6b40b98
Download 4ab7def Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T19:43:03+01:00 Download d73927a
Download d0cc112 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:13:35+01:00 Download d9a765c
Download b8ab5c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:02:53+01:00 Download 25f5119
Download 40f78a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:53+01:00 Download 7e78bbf
Download 5d3c693 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T19:32:57+01:00 Download 6073c5d
Download 4e8fc40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T17:03:48+01:00 Download e10ffc2
Download e10ffc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T03:54:20+01:00
Download 9a49a8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 6 2019-12-07T22:08:06+01:00
Download 9cde24b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T09:44:03+01:00
Download 044a3eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T22:03:01Z

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

Trying to find witnesses for program (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3166b61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:29:48
Download 672848a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T00:00 CET (sv-comp)
Download 4bac312 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 6 2018-12-10T19:12:35+01:00
Download 18d4f16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T09:50:45+01:00
Download 1479d2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:00:14+01:00 Download 4bac312
Download acebfe6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:26:36+01:00 Download 52f83cf
Download 0218470 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T17:28:08+01:00 Download f1aa300
Download 7584a69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:29:13+01:00 Download 3166b61
Download d299628 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T06:13:32+01:00 Download 18d4f16
Download f73d109 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:48:57+01:00 Download 0c068dc
Download d385bc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:45:58+01:00 Download 01f346e
Download de1e836 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:38:00+01:00 Download 672848a
Download bcd1b6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:57+01:00 Download afd39fe
Download d7122ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:45:33+01:00 Download d4fe739
Download 44c702c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:25:34+01:00 Download c394fae
Download 81cf568 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:17:19+01:00 Download 666ac15
Download d04eb63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:41:11+01:00 Download 92b8d48
Download d4fe739 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T06:10:39+01:00

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

Trying to find witnesses for program (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a6cc4b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T15:34:54+01:00
Download 8d75101 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-01T22:27:15+01:00
Download 74db385 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-03T04:52Z
Download 15aae91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T03:33:19.317965
Download 737077b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T19:28:32.819419
Download d8e385a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-03T01:36:48+01:00
Download 7074954 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T20:28:44+01:00
Download f9c978b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T07:03:29+01:00 afab9e0
Download b509b9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T03:58:33+01:00 1de58a5
Download 55f7483 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T02:03:58+01:00 4e7b27a
Download 2b0b32f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T07:55:53+01:00 a801740
Download 742730a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:32:03+01:00 0f89a5e
Download 9e73d62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:13:58+01:00 0911901
Download 9bf93ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T07:02:07+01:00 25c2033
Download 20da602 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:59:49+01:00 e7c8dec
Download 12ba43c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T05:33:59+01:00 db5e4d5
Download 271a307 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T02:04:35+01:00
Download 3f8cf17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 6 2017-11-30T13:34 CET (sv-comp)
Download 65cde04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T16:28Z
Download eb8566d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 8 2017-11-30T22:30 CET (sv-comp)

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

Trying to find witnesses for program (5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501, sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/zonotope_tight_true-unreach-call_true-termination.c, 5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5f42a66896ae1e95e2a409a23d04a83381e01bc12f88e0844abc46f432042501.json

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