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/simple_true-unreach-call2_true-termination.i
programSHA df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c
witnessName results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.simple_true-unreach-call2_true-termination.i.files/witness.graphml
witnessSHA 2fa2183593849667c0f2cb80e1bb3a37d655afdac81e2a85a733ecc960a76352

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T10:52:53+01:00
producer CPAchecker 1.7-svn 29852
program-sha256 df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c
programfile ../../sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i
programhash df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/2fa2183593849667c0f2cb80e1bb3a37d655afdac81e2a85a733ecc960a76352.graphml
witness-sha256 2fa2183593849667c0f2cb80e1bb3a37d655afdac81e2a85a733ecc960a76352
witness-size 4934
witness-type correctness_witness

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

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

Trying to find witnesses for program (df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c, sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i).

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i, df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c.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 (df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c, sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i).

Found 17 witnesses for program sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i, df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 25a5920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T09:22 CET (sv-comp)
Download edfc286 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T06:34:04
Download c8a6200 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T15:34:24+01:00
Download ca2750d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T19:45:28+01:00 Download f4a5060
Download f5ee2c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T21:06:33+01:00 Download 5e86081
Download c6bf017 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:23:00+01:00 Download ad7ddd6
Download 210f24d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:50:49+01:00 Download d898a4d
Download 74a800c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:31:22+01:00 Download 2a297d7
Download 31fdb14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:07:11+01:00 Download 25a5920
Download fcf16de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:30:36+01:00 Download edfc286
Download 721c880 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T06:11:07+01:00 Download c8a6200
Download dcc7ddb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:08+01:00 Download 4d395ed
Download 16d1ba0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:32+01:00 Download 2da653f
Download cd9e8ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:06:31+01:00 Download 2fa2183
Download 3e1b356 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:18:54+01:00 Download e673e19
Download 2fa2183 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T10:52:53+01:00
Download 6b5c031 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T09:30 CET (sv-comp)

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

Trying to find witnesses for program (df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c, sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i).

Found 28 witnesses for program sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i, df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4d395ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:38 CET (sv-comp)
Download 7565b02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T05:20Z
Download 63d40a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T16:05 CET (sv-comp)
Download d75b1b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T21:34 CET (sv-comp)
Download d282024 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 4 2017-12-02T18:13Z
Download 0f061d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T19:43 CET (sv-comp)
Download 36518c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-12-02T22:06:37+01:00
Download 7dfdeaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T05:26:54+01:00
Download b8e47e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T07:03:35+01:00 76f267d
Download 7e5086b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:10:43+01:00 36f9959
Download 3c46bd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:38:45+01:00 5d451ed
Download a96d25e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:30:19+01:00 f3566c5
Download b81267d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:06:25+01:00 043cb1d
Download c1ba7a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T15:27:03+01:00 07eee88
Download 1c48728 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:11:57+01:00 5c237a1
Download c79a43f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:12:08+01:00 cb57081
Download be9cf33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:54+01:00 b50a32e
Download 22648e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:37:58+01:00 df53ac0
Download 98a4ff1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:08:37+01:00 c99da2f
Download a34b37f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:17:19+01:00 7fb1c5d
Download e824fa7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:47:47+01:00 f9d114e
Download 617cc7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T01:30:50+01:00
Download ae32152 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 7 2017-11-30T11:42:47+01:00
Download 1204f67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T14:19:35+01:00
Download 02eb8f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T11:27:34+01:00
Download ac976e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T11:41Z
Download 80bdf29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-11-30T16:09 CET (sv-comp)
Download 49a05c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T16:19 CET (sv-comp)

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

Trying to find witnesses for program (df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c, sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/simple_true-unreach-call2_true-termination.i, df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/df3991ef7f83300c56d9945b7c0397335c8155777ed061e9c8a68eeb50545a5c.json

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