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/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c
programSHA 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-nooverflow.recHanoi03_true-unreach-call_true-no-overflow_true-termination.c.files/witness.graphml
witnessSHA fd8d150f4b43dff6083a764a39dcd396b5c156c13d54a764b178397a32cb2172

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T18:01:38.965858
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c
programhash 887ada769b510ae5d273618525924110908f2b5f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/fd8d150f4b43dff6083a764a39dcd396b5c156c13d54a764b178397a32cb2172.graphml
witness-sha256 fd8d150f4b43dff6083a764a39dcd396b5c156c13d54a764b178397a32cb2172
witness-size 3412
witness-type correctness_witness

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

Trying to find witnesses for program (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.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 (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.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 (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.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 (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.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 (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 13 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ec52fc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2019-12-03T22:43 CET (comp)
Download 88ae7c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:52 CET (comp)
Download 25af3ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:27:48+01:00 Download 5120245
Download 786ae07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:25+01:00 Download 4360a60
Download fd40637 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:36:44+01:00 Download e87e34b
Download fb97118 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T19:45:08+01:00 Download 3d17556
Download 2b0c9b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T01:43:49+01:00 Download 961159d
Download 4386ec9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:12:46+01:00 Download 85bd8d2
Download 482b6d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:39+01:00 Download 88ae7c8
Download 56ea4ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T19:55:21+01:00 Download aca9e6e
Download 8f9225e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T17:18:14+01:00 Download 65b5c5d
Download 65b5c5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 10116 2019-11-30T14:46:46+01:00
Download d1f0130 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:03 CET (comp)

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

Trying to find witnesses for program (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 23 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 57bd05f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T12:15 CET (sv-comp)
Download fa1169d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-07T06:58 CET (sv-comp)
Download d11d288 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 6686 2018-12-05T20:51:58+01:00
Download 458bcbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T09:37 CET (sv-comp)
Download 2962249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T16:39:34
Download b5aa1fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T14:02 CET (sv-comp)
Download eeda06d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 11518 2018-12-07T18:20:14+01:00
Download d63e9e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T21:06:35+01:00 Download 4d98922
Download e70ef0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T19:49:13+01:00 Download 0cab13c
Download a0893b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T17:28:10+01:00 Download d8fbe70
Download 2b5a15f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:22:22+01:00 Download 458bcbe
Download ac9b2e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:45:30+01:00 Download 2962249
Download b914535 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:09:46+01:00 Download eeda06d
Download 2af7d7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:39:42+01:00 Download 6043f02
Download 3742f50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T01:51:10+01:00 Download a4dd188
Download a212b1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:33:51+01:00 Download b5aa1fa
Download a99da9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:21+01:00 Download 7faced7
Download db10e10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:46:03+01:00 Download de8d1c5
Download abaa5db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:27:40+01:00 Download ac3d200
Download b3f4883 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:02:29+01:00 Download bfc1c68
Download de8d1c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11518 2018-12-06T01:29:31+01:00
Download dde8861 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T20:25 CET (sv-comp)
Download 6a55796 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T14:11 CET (sv-comp)

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

Trying to find witnesses for program (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 32 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 05aa878 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:20 CET (sv-comp)
Download 5f1c4c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 4 2017-12-02T01:02 CET (sv-comp)
Download 9f2670d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T17:51:40.286186
Download 2407e94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-02T06:08:57.826117
Download 939b57e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 6 2017-12-01T14:24 CET (sv-comp)
Download c59b79b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 59 2017-12-01T12:04 CET (sv-comp)
Download f4c261c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 9 2017-12-03T10:37Z
Download 478a532 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T23:51:47+01:00
Download e4ca55f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T02:02:46+01:00
Download 0cb8be6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T09:56:36+01:00
Download e88c6e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness VIAP 6 2017-12-03T03:53 CET (sv-comp)
Download af43d91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T15:33 CET (sv-comp)
Download 0b301e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T21:10 CET (sv-comp)
Download 6cc9bbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 7 2017-12-02T11:42Z
Download 758f2ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:25:36.725027
Download 16e0d5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:49:26.232252
Download f784718 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:08:44.509725
Download 750ac2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T19:35:34.125749
Download b51f14d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T21:05 CET (sv-comp)
Download 9d7598c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-01T05:30:12+01:00
Download a71979e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:22:01+01:00 c2d6dad
Download a4d1833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T01:49:17+01:00 60abe29
Download 7c880a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T01:16:24+01:00 7abb648
Download 87d082c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:51:42+01:00 3bb8f5f
Download 9b15d0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T08:47:49+01:00 c5a2461
Download 88f08e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:29:03+01:00 40ab310
Download 294b991 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:13:48+01:00 543dfec
Download cc24296 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:13:30+01:00 7ef13d3
Download ad882c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T04:57:26+01:00 3f2b286
Download ac99564 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 29 2017-12-01T00:10 CET (sv-comp)
Download 4e4defd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 7 2017-12-02T17:09Z
Download 6920021 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 29 2017-12-01T13:04 CET (sv-comp)

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

Trying to find witnesses for program (6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b, sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c, 6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6b73c20c48b2d03f023274d03db6af85302968fe4474c173fe1e0b59911c2c5b.json

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