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_i5_o5_false-unreach-call_true-termination.c
programSHA 54b0741ef8bba95c8991877c95f07e67695b73da621619bcc97f415474c48c0c
witnessName results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.id_i5_o5_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA b015cfc9ce8cd9d92ab6c46e90e01d3a088650ec7477b0eefd39adbc24a0359d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T07:03 CET (sv-comp)
producer Symbiotic
program-sha256 54b0741ef8bba95c8991877c95f07e67695b73da621619bcc97f415474c48c0c
programfile /tmp/vcloud-vcloud-master/worker/working_dir_f7926aa7-dca1-4975-a638-eee5d3cc5db9/sv-benchmarks/c/recursive-simple/id_i5_o5_false-unreach-call_true-termination.c
programhash bd8a40b9ab0ccbf5be4fcc211d81cb04996473fb
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b015cfc9ce8cd9d92ab6c46e90e01d3a088650ec7477b0eefd39adbc24a0359d.graphml
witness-sha256 b015cfc9ce8cd9d92ab6c46e90e01d3a088650ec7477b0eefd39adbc24a0359d
witness-size 801
witness-type violation_witness

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

Trying to find witnesses for program (54b0741ef8bba95c8991877c95f07e67695b73da621619bcc97f415474c48c0c, sv-benchmarks/c/recursive-simple/id_i5_o5_false-unreach-call_true-termination.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f09f039 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 10:12:35
Download c9644d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 7 2019-12-04T00:30 CET (comp)
Download f18b9a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T21:54:00+01:00 Download d50b354
Download 0b9dd00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T21:40:14+01:00 Download bacabc6
Download dc6144a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T21:09:18+01:00 Download f09f039
Download 97e1f19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T20:54:20+01:00 Download 3c04efd
Download 8104d1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T20:44:52+01:00 Download 1896f4a
Download e176e27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-08T00:26:16+01:00 Download f8c567d
Download 40f4ac1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-07T21:16:47+01:00 Download b79e697
Download d38458d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-06T02:38:54+01:00 Download 1ccf1d1
Download 359dbe9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-04T02:58:22+01:00 Download c9644d7
Download b497007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-03T08:57:06+01:00 Download d8ab65c
Download 18925b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-03T08:08:32+01:00 Download ef0b5ce
Download ef0b5ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 10 2019-11-30T04:37:22+01:00
Download d50b354 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 10 2019-12-01T12:49:41+01:00
Download bc86001 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:51:17+01:00 Download defd5ee
Download 2dfa54c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:21:30+01:00 Download 33552ad
Download 9acc906 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:15 CET (comp)

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

Trying to find witnesses for program (54b0741ef8bba95c8991877c95f07e67695b73da621619bcc97f415474c48c0c, sv-benchmarks/c/recursive-simple/id_i5_o5_false-unreach-call_true-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b7e809e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T10:57 CET (sv-comp)
Download 54fc6bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T05:48:00
Download 07bcafe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 7 2018-12-07T06:44 CET (sv-comp)
Download 9b885f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 11 2018-12-07T08:02:42+01:00
Download 2d8da52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-10T10:48:46+01:00 Download a6c37c4
Download 0b6677c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T21:23:37+01:00 Download 10a0e78
Download 071bd32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:53:08+01:00 Download b686024
Download d512928 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:39:25+01:00 Download a3e6eb0
Download 3fae8fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:25:41+01:00 Download 9959cd0
Download cd3a068 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T18:20:12+01:00 Download 65d15f2
Download d494e0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T23:44:32+01:00 Download b7e809e
Download ac59236 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T22:09:43+01:00 Download 54fc6bc
Download d5d0ed3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T09:01:08+01:00 Download 9b885f1
Download eb08f98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T04:58:38+01:00 Download 76986c4
Download 3fa9786 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T04:35:45+01:00 Download a6c37c4
Download 7e0b990 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-07T18:48:33+01:00 Download d9e5a04
Download 3edc18d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-07T17:45:23+01:00 Download 07bcafe
Download ce362d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-07T01:06:54+01:00 Download 24a36e4
Download d394018 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-06T10:18:15+01:00 Download 92e2a03
Download 2e40eaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:48:40+01:00 Download 9fa3b2b
Download 532f54f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:16:44+01:00 Download 51cffb5
Download 9fa3b2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-06T00:21:29+01:00
Download 9ad95c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:34:48+01:00 Download 20f0f70
Download 4e0a477 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:00:13+01:00 Download 80d650a
Download 87a3db7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T04:14 CET (sv-comp)
Download 3a0a7ae Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T21:27 CET (sv-comp)

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

Trying to find witnesses for program (54b0741ef8bba95c8991877c95f07e67695b73da621619bcc97f415474c48c0c, sv-benchmarks/c/recursive-simple/id_i5_o5_false-unreach-call_true-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5ffcf40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:07 CET (sv-comp)
Download 3e87c4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 7 Sat Dec 2 23:25:12 2017
Download 10a0e78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 9 2017-12-03T03:47 CET (sv-comp)
Download c80febf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 9 2017-12-03T04:40Z
Download b015cfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T07:03 CET (sv-comp)
Download fc8c1e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T20:14 CET (sv-comp)
Download 8c2a0bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 9 2017-12-02T08:00Z
Download c1ae41e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T15:30:19.486875
Download 0eff5d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T08:05:34.199491
Download 81bbf19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T21:44 CET (sv-comp)
Download 9ebbc7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T04:14 CET (sv-comp)
Download a1e2c63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 10 2017-11-30T21:16:40+01:00
Download 72886d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T21:27:47+01:00
Download c8b2b91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T19:38:31+01:00
Download 7b2280e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T11:15:23+01:00
Download b1eb392 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 7 2017-11-30T16:30 CET (sv-comp)
Download e52cb7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 9 2017-12-02T17:20Z
Download 15d7f32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:19:56.078545
Download f19d2f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:20:25.811082
Download 33ecf53 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 7 2017-12-01T17:27 CET (sv-comp)

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

Trying to find witnesses for program (54b0741ef8bba95c8991877c95f07e67695b73da621619bcc97f415474c48c0c, sv-benchmarks/c/recursive-simple/id_i5_o5_false-unreach-call_true-termination.c).

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

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