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/loop-lit/gcnr2008_false-unreach-call_false-termination.i
programSHA a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
witnessName results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.gcnr2008_false-unreach-call_false-termination.i.files/witness.graphml
witnessSHA a83c990665fcf5c303e263356fd3e6798a4c49540d2f1f4ad239fd361ff1de93

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T18:22 CET (sv-comp)
producer CBMC
program-sha256 a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
programfile ../../sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i
programhash 153d29cc59a928b964d34eac87caede5c68a6fb0
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a83c990665fcf5c303e263356fd3e6798a4c49540d2f1f4ad239fd361ff1de93.graphml
witness-sha256 a83c990665fcf5c303e263356fd3e6798a4c49540d2f1f4ad239fd361ff1de93
witness-size 4427
witness-type violation_witness

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

Trying to find witnesses for program (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.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 (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.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 (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.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 (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.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 (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 12 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 50c340f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 13:32:44
Download 03cd2ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-03T21:45 CET (comp)
Download 9a55a44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T21:56:14+01:00 Download 1f713f7
Download c17e593 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T21:40:03+01:00 Download 5d69cae
Download 709ca45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T21:09:24+01:00 Download 50c340f
Download bbdba6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-08T01:52:19+01:00 Download 12507e6
Download ec29953 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-08T00:26:43+01:00 Download c0bc91b
Download 8b0c32e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T21:16:57+01:00 Download 9847e70
Download 405071a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-03T08:09:38+01:00 Download 12c74f0
Download 12c74f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T04:49:33+01:00
Download 12507e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 7 2019-12-07T11:49:48+01:00
Download 5d69cae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 7 2019-12-01T11:54:43+01:00

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

Trying to find witnesses for program (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 14 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8f89f3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T12:51 CET (sv-comp)
Download 3847f75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T01:34:28
Download b7fef84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 182 2018-12-07T09:52 CET (sv-comp)
Download e992b8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 7 2018-12-10T18:48:32+01:00
Download ecc24bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-08T00:11:32+01:00
Download ee2be8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:34:51+01:00 Download e992b8b
Download 6448b8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:10+01:00 Download 411a220
Download aa122d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:39:32+01:00 Download e34f52b
Download 12fe01a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:25:16+01:00 Download 16ce83b
Download bb35c91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 313 2018-12-09T18:19:54+01:00 Download 9aba235
Download ab70617 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T08:18:29+01:00 Download ecc24bd
Download f574131 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 313 2018-12-07T17:44:04+01:00 Download b7fef84
Download 7bbdf85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:48:47+01:00 Download a09f3ca
Download a09f3ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-05T17:01:06+01:00

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

Trying to find witnesses for program (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 19 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ee2a156 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:37 CET (sv-comp)
Download aaee5c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 165 2017-12-03T03:54 CET (sv-comp)
Download aadc04b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-02T19:36Z
Download 3a3a816 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:30 CET (sv-comp)
Download b89fe10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T21:28 CET (sv-comp)
Download 3967602 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 5 2017-12-02T19:33Z
Download dcab3a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T22:37:37.820449
Download 7f2f553 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T10:52:09.911566
Download 5b50106 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T21:10 CET (sv-comp)
Download dedf4a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T20:22 CET (sv-comp)
Download 0bd5c5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 7 2017-12-03T03:37:11+01:00
Download 1c0dccf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T17:13:16+01:00
Download db203d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 15 2017-11-30T18:23:26+01:00
Download c8a2948 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T21:05:13+01:00
Download 1d625d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T23:37:07+01:00
Download a83c990 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T18:22 CET (sv-comp)
Download 53c902c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T10:45Z
Download 291c425 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-12-01T03:02 CET (sv-comp)
Download 7064733 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 6 2017-12-03T11:13Z

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

Trying to find witnesses for program (a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3, sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-lit/gcnr2008_false-unreach-call_false-termination.i, a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a31d2b9103ae1a198e836c02ae8f6e59d7d5eb81ae3910daedabb3fb99e0f8d3.json

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