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_o200_false-unreach-call_true-termination_true-no-overflow.c
programSHA 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
witnessName results-validated/cpa-seq-validate-violation-witnesses-depthk.2018-12-06_1002.logfiles/sv-comp19_prop-reachsafety.id_o200_false-unreach-call_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA b5c0391a0a32ec739f334792844e6bc8d8f75eb922687feca58f260490a8e8a7

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T10:19:24+01:00
inputwitnesshash 8343699bd16d0d1ce433c178b1accb085095c7ff1117462f48ebda554906deae
producer CPAchecker 1.7-svn 29852
program-sha256 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
programfile ../../sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c
programhash 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b5c0391a0a32ec739f334792844e6bc8d8f75eb922687feca58f260490a8e8a7.graphml
witness-sha256 b5c0391a0a32ec739f334792844e6bc8d8f75eb922687feca58f260490a8e8a7
witness-size 4892
witness-type correctness_witness

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

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

Trying to find witnesses for program (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.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 (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.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 (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.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 (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.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 (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 12 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f7c7414 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-11-30T09:22:18+01:00
Download 1b0e620 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T00:31:01+01:00
Download 204b7e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 09:11:38
Download fada311 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 224 2019-12-11T21:56:27+01:00 Download 3a1c3b4
Download 658b779 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 224 2019-12-11T21:09:45+01:00 Download 204b7e0
Download e504cd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 222 2019-12-11T20:44:31+01:00 Download b2b14d7
Download c3553f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 222 2019-12-06T02:40:51+01:00 Download 5aaf9d3
Download 0a0584b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 224 2019-12-03T08:09:57+01:00 Download 3ac0f01
Download 3ac0f01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 222 2019-11-29T18:17:07+01:00
Download 3a1c3b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 222 2019-12-01T18:18:12+01:00
Download 7ce5c13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:55:17+01:00 Download 4d80f76
Download c1d6068 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:51:49+01:00 Download e9240d1

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

Trying to find witnesses for program (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 17 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e11964f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T16:58 CET (sv-comp)
Download b115e9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:26:20
Download 5db9c9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T07:58:57+01:00
Download eef4294 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:30:58+01:00
Download 7463eb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T08:43 CET (sv-comp)
Download 66c8702 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T02:20:43
Download 09a9b9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 107 2018-12-07T15:33 CET (sv-comp)
Download afc6a5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 222 2018-12-08T02:00:44+01:00
Download 776f615 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 224 2018-12-09T21:23:49+01:00 Download c0854a9
Download 2740840 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 224 2018-12-08T23:44:11+01:00 Download 7463eb9
Download 539c267 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 224 2018-12-08T08:36:37+01:00 Download afc6a5f
Download 259f9a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 222 2018-12-07T18:39:19+01:00 Download fff7391
Download 7192912 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 224 2018-12-06T09:48:20+01:00 Download 175f542
Download 175f542 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 222 2018-12-06T06:44:29+01:00
Download dad0b05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:08:40+01:00 Download 83eec41
Download b5c0391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:19:24+01:00 Download 8343699
Download b655132 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:17 CET (sv-comp)

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

Trying to find witnesses for program (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 19 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 82a3791 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2017-12-03T07:44Z
Download f0ebc9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:29 CET (sv-comp)
Download e924b4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2017-12-03T10:20Z
Download f072e56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 5 2017-12-01T13:37 CET (sv-comp)
Download d97973e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:18:07+01:00
Download 56ce6f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:30Z
Download b469fa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:57 CET (sv-comp)
Download 54ddab3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 4 2017-12-03T04:02 CET (sv-comp)
Download 67a15b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:46 CET (sv-comp)
Download 165b235 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T19:55 CET (sv-comp)
Download 45bd59f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T21:20:11.173762
Download 91cd705 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T09:04:31.318832
Download 1f2cbd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 100 2017-12-01T00:24:47+01:00
Download ffda857 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 222 2017-11-30T23:43:30+01:00
Download f6ba381 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T11:23:23+01:00
Download 049a201 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T15:44:22+01:00
Download 7555cf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T22:35:15+01:00
Download a9a636f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 139 2017-11-30T21:58 CET (sv-comp)
Download b38951c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T16:14 CET (sv-comp)

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

Trying to find witnesses for program (0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31, sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c, 0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0a3e49d7d484afd468681cd9c74173f2e24356a8a6338805bb0a6af8793d3c31.json

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