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-acceleration/diamond_true-unreach-call2.i
programSHA 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
witnessName results-validated/cpa-seq-validate-correctness-witnesses-depthk.2018-12-06_0926.logfiles/sv-comp19_prop-reachsafety.diamond_true-unreach-call2.i.files/witness.graphml
witnessSHA 898a343716aba4f980869e0a7f0c8cebe4d47a1625f47731e380c4f3121d6e27

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:28:53+01:00
inputwitnesshash 3f81a963680c05acc3e27d8496172870df3fe5fd35f7096c25c9b7388f2a5612
producer CPAchecker 1.7-svn 29852
program-sha256 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
programfile ../../sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i
programhash 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/898a343716aba4f980869e0a7f0c8cebe4d47a1625f47731e380c4f3121d6e27.graphml
witness-sha256 898a343716aba4f980869e0a7f0c8cebe4d47a1625f47731e380c4f3121d6e27
witness-size 10094
witness-type correctness_witness

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

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

Trying to find witnesses for program (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.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 (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.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 (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.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 (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.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 (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.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 '19

Trying to find witnesses for program (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 20 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 577618c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:27 CET (sv-comp)
Download f8a0d14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:01:49
Download 665c497 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T22:45 CET (sv-comp)
Download d1d41d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 11 2018-12-08T03:46:24+01:00
Download 1946746 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-10T19:47:50+01:00 Download f10b316
Download 6680645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-09T21:06:14+01:00 Download 707b512
Download 8fbc043 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:18:44+01:00 Download bbd0e88
Download a4848e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-09T19:55:59+01:00 Download 1e80b38
Download c579d56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T17:25:34+01:00 Download 669b04a
Download ea52fde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T22:58:39+01:00 Download 577618c
Download 4793583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T21:41:55+01:00 Download f8a0d14
Download b250c45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T06:26:19+01:00 Download d1d41d7
Download aaf17c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T02:52:58+01:00 Download 4d1b457
Download d223f7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T01:53:21+01:00 Download 805507d
Download 71daadd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-07T16:38:38+01:00 Download 665c497
Download 898a343 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:28:53+01:00 Download 3f81a96
Download 4a47d39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T08:45:29+01:00 Download 300ceb0
Download 5e218a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T08:22:47+01:00 Download bd11abf
Download 6f72689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T07:44:43+01:00 Download ae11fa4
Download 300ceb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T02:57:38+01:00

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

Trying to find witnesses for program (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 28 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ac71f6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 13 2017-12-03T01:38Z
Download 8268b28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-01T23:37 CET (sv-comp)
Download 3903d8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 5 2017-12-01T20:24 CET (sv-comp)
Download e1962a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T22:21:00.999305
Download ae1d39e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T09:12:08.715383
Download 4d0bfad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 11 2017-12-03T02:33:03+01:00
Download 16f2dda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T16:45:44+01:00
Download 0a6f12d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T07:01:00+01:00 6f3666d
Download 9f967b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-03T04:21:41+01:00 9e441b6
Download a6ca414 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T00:02:11+01:00 f04c81d
Download 871f3d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-02T19:54:43+01:00 b9a00ae
Download ce879b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-02T14:27:55+01:00 ba6b6da
Download 481b9ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-02T08:47:40+01:00 aeeb8e8
Download 3322465 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T22:36:46+01:00 0445af5
Download ecf2b23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T22:07:14+01:00 ebf9cd8
Download 09a940b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T08:14:01+01:00 7e68706
Download 6eb6913 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T07:17:42+01:00 d402067
Download 184f3f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T07:14:47+01:00 962b074
Download d85b611 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T06:25:33+01:00 f2a8437
Download 09c6283 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T06:16:35+01:00 01f9e75
Download dacf1a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T05:21:51+01:00 f045123
Download 6c43fc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-11-30T13:00:16+01:00
Download b772ea8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 22 2017-11-30T15:26:17+01:00
Download 4fc43a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 10 2017-11-30T22:46:58+01:00
Download 067273f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 10 2017-12-01T22:15:37+01:00
Download c29ce9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 57 2017-12-01T02:10 CET (sv-comp)
Download 1dd1f5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 13 2017-12-02T18:16Z
Download 3cbeb4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 74 2017-11-30T23:28 CET (sv-comp)

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

Trying to find witnesses for program (135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call2.i, 135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/135f94b2561f066cad6a712a06e4f94426311637e4996f203f4d887969619361.json

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