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/eca-rers2012/Problem05_label39_false-unreach-call.c
programSHA 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
witnessName results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-reachsafety.Problem05_label39_false-unreach-call.c.files/witness.graphml
witnessSHA 0d9e276a3dae0a98dc5511c9233f8a2da5e8ac3f3d945970541939609a12067a

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:49:09+01:00
inputwitnesshash d987e93d785bb5bdeef9932051dc78edb11f6275b21015878de1bbff990b7319
producer CPAchecker 1.7-svn 29852
program-sha256 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
programfile ../../sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c
programhash 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0d9e276a3dae0a98dc5511c9233f8a2da5e8ac3f3d945970541939609a12067a.graphml
witness-sha256 0d9e276a3dae0a98dc5511c9233f8a2da5e8ac3f3d945970541939609a12067a
witness-size 6650377
witness-type violation_witness

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

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

Trying to find witnesses for program (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.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 (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.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 (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.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 (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.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 (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 8 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0569140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 19:34:23
Download 8dd2545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6650 2019-12-11T21:42:48+01:00 Download 2125877
Download 8ebc8d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6650 2019-12-11T21:09:17+01:00 Download 0569140
Download 16a97ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6650 2019-12-11T20:54:35+01:00 Download d9a8cfe
Download 7d3898f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6650 2019-12-11T20:44:51+01:00 Download 4ee4d78
Download 05eef31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6650 2019-12-03T08:08:42+01:00 Download cffb39c
Download cffb39c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6754 2019-11-30T03:28:58+01:00
Download 2125877 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6714 2019-12-01T00:47:11+01:00

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

Trying to find witnesses for program (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 7 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download be09369 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6754 2018-12-08T03:40:03+01:00
Download cce6e70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6685 2018-12-10T20:39:01+01:00 Download 1fc7c59
Download 7a3adee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6650 2018-12-09T18:21:26+01:00 Download a2ffaf2
Download f240034 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6650 2018-12-08T08:30:16+01:00 Download be09369
Download 0e6a17a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6651 2018-12-08T05:00:30+01:00 Download 8d7fd1b
Download 0d9e276 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6650 2018-12-06T09:49:09+01:00 Download d987e93
Download d987e93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6754 2018-12-05T11:47:31+01:00

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

Trying to find witnesses for program (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f1e809b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T14:12:12.396976
Download cd4866d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T19:02:38.603979
Download 7df50f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 3698 2017-11-30T12:29:45+01:00
Download f2fb05c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 2436 2017-11-30T18:16 CET (sv-comp)
Download 4e5d4c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 2438 2017-12-01T01:28 CET (sv-comp)

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

Trying to find witnesses for program (6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2, sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label39_false-unreach-call.c, 6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6462ca8b00975ff27d1c436997792bd847b86537e0166ee8221fbd8a5974ddd2.json

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