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/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c
programSHA 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
witnessName results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-reachsafety.id_i20_o20_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 037bd94939a58b7a0e2f86fa9624d1e732b6f1f19e4b59fb758115ccb06438e0

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/037bd94939a58b7a0e2f86fa9624d1e732b6f1f19e4b59fb758115ccb06438e0.json

Key Value
architecture 32bit
creationtime 2018-12-06T09:48:57+01:00
inputwitnesshash 64c2eb914101e974a141bfadf63a65dcc369d6e27c813ea5c79cf9fa1910c76b
producer CPAchecker 1.7-svn 29852
program-sha256 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
programfile ../../sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c
programhash 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/037bd94939a58b7a0e2f86fa9624d1e732b6f1f19e4b59fb758115ccb06438e0.graphml
witness-sha256 037bd94939a58b7a0e2f86fa9624d1e732b6f1f19e4b59fb758115ccb06438e0
witness-size 26695
witness-type violation_witness

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

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

Trying to find witnesses for program (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.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 (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.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 (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.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 (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.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 (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6855ac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 00:02:06
Download ffd281f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 13 2019-12-03T23:49 CET (comp)
Download b7e6f30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T21:49:16+01:00 Download bc062dd
Download 8f9653d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T21:40:56+01:00 Download c88de69
Download dce008a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T21:09:02+01:00 Download 6855ac2
Download 0ad6de8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 26 2019-12-11T20:55:19+01:00 Download 7efa299
Download 3aca6bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T20:44:26+01:00 Download dfa0a8c
Download 93ef2b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-08T00:27:24+01:00 Download 7375bb9
Download cc1659d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-07T21:16:34+01:00 Download 0f209da
Download 14b00c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 26 2019-12-06T02:43:11+01:00 Download 553ba19
Download 52e61cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-04T02:58:28+01:00 Download ffd281f
Download cc8b1a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 26 2019-12-03T08:57:12+01:00 Download 0da2f68
Download 72aae60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 27 2019-12-03T08:10:10+01:00 Download dc08479
Download dc08479 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 26 2019-11-30T13:23:23+01:00
Download c88de69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 26 2019-12-01T07:35:06+01:00
Download 0b96429 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:52:20+01:00 Download 3ec2881
Download 49f8115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:20:14+01:00 Download ab97f32
Download 9d4b760 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:12 CET (comp)

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

Trying to find witnesses for program (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 26 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1c93fc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T03:53 CET (sv-comp)
Download 9cc2bdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T04:31:28
Download bd81da4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 14 2018-12-06T21:06 CET (sv-comp)
Download e159bac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 26 2018-12-06T20:24:14+01:00
Download 8f02c97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-10T10:48:54+01:00 Download 0e176e5
Download 92c4d29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-09T21:23:40+01:00 Download 2a32cad
Download 66d3f49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-09T20:53:13+01:00 Download 9d366e5
Download cd85550 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-09T20:39:43+01:00 Download 8368b19
Download f09dadb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-09T20:30:20+01:00 Download 022b8f2
Download 4bfeaf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-09T17:59:13+01:00 Download 38a0181
Download b6888d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-08T23:43:03+01:00 Download 1c93fc0
Download 7f9677f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-08T22:07:26+01:00 Download 9cc2bdc
Download 854721e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-08T08:09:52+01:00 Download e159bac
Download dc0f4e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-08T04:57:37+01:00 Download 20f2438
Download 06ce3ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-08T04:36:58+01:00 Download 0e176e5
Download 7d2fade Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-07T18:19:14+01:00 Download 66ba1c1
Download 56329d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-07T17:45:40+01:00 Download bd81da4
Download 6587214 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-07T01:06:31+01:00 Download 2781c40
Download 8dc8260 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-06T10:20:12+01:00 Download 0203a90
Download 037bd94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-06T09:48:57+01:00 Download 64c2eb9
Download 11451b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 27 2018-12-06T09:16:49+01:00 Download 03b13ca
Download 64c2eb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-06T07:23:56+01:00
Download a6821f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:36:03+01:00 Download 3e87a19
Download 765a1e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:18:47+01:00 Download 5795185
Download e8533e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T09:08 CET (sv-comp)
Download 84922d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T11:13 CET (sv-comp)

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

Trying to find witnesses for program (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4056d83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:26 CET (sv-comp)
Download ae30f6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 16 Sat Dec 2 20:12:26 2017
Download 2a32cad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 20 2017-12-03T03:48 CET (sv-comp)
Download 0348016 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 21 2017-12-02T18:41Z
Download 5b558c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:01 CET (sv-comp)
Download c242f90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T21:15 CET (sv-comp)
Download d919de4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 21 2017-12-02T14:05Z
Download b38715e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T04:08:27.399540
Download 8e4ee58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T19:26:15.673167
Download f33fb91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 8 2017-12-01T16:05 CET (sv-comp)
Download 016276a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 8 2017-12-01T04:13 CET (sv-comp)
Download 6dd39ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 26 2017-11-30T16:07:42+01:00
Download 6ac09cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T14:44:43+01:00
Download 4e76738 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T00:18:17+01:00
Download b8d01b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T03:42:41+01:00
Download eedb775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 17 2017-11-30T22:57 CET (sv-comp)
Download 679f72a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 21 2017-12-02T18:49Z
Download e99537e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:27:22.746920
Download ba5872f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:00:56.045420
Download 02a84e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 15 2017-12-01T19:14 CET (sv-comp)

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

Trying to find witnesses for program (21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b, sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i20_o20_false-unreach-call_true-termination.c, 21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/21a977dc01fbb676ffbd104991f6d1e698de7db9cfedad64decaf2424e4fc66b.json

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