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/Problem02_label43_false-unreach-call_false-termination.c
programSHA 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
witnessName results-validated/cpa-seq-validate-violation-witnesses-2ls.2018-12-06_0936.logfiles/sv-comp19_prop-reachsafety.Problem02_label43_false-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 3d96ea94d368a96cce47304653ef0fdc098b97259aa9255bbe1a1a8fedd9090d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:42:10+01:00
inputwitnesshash c45ef06237a1a8fe79492883a5fe9546c6705bb76439481cf3a5b399f857f835
producer CPAchecker 1.7-svn 29852
program-sha256 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
programfile ../../sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c
programhash 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3d96ea94d368a96cce47304653ef0fdc098b97259aa9255bbe1a1a8fedd9090d.graphml
witness-sha256 3d96ea94d368a96cce47304653ef0fdc098b97259aa9255bbe1a1a8fedd9090d
witness-size 280002
witness-type correctness_witness

This witness was created for this program (cf. table above, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b).

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

Trying to find witnesses for program (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.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 (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.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 (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.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 (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.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 (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6539048 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 18:20:36
Download 0716d76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 32 2019-12-03T22:06 CET (comp)
Download 708a71e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 125 2019-12-11T21:49:30+01:00 Download d7708f9
Download 56697cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 90 2019-12-11T21:45:17+01:00 Download 4a75eb5
Download 85a9e93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 90 2019-12-11T21:09:02+01:00 Download 6539048
Download 9fc6fb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 90 2019-12-11T20:55:27+01:00 Download d913e83
Download 3f21aa3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 90 2019-12-11T20:44:26+01:00 Download cc4d489
Download 8e974df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 90 2019-12-08T01:51:22+01:00 Download 24b0b68
Download 3f21e05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 125 2019-12-08T00:26:30+01:00 Download fa22edd
Download 1362f71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 125 2019-12-07T21:17:37+01:00 Download c6f87eb
Download c970907 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 111 2019-12-04T02:58:25+01:00 Download 0716d76
Download e04e49b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 90 2019-12-03T08:08:45+01:00 Download 5e10bd5
Download 5e10bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 89 2019-11-30T14:48:02+01:00
Download 4a75eb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 89 2019-11-30T23:03:26+01:00
Download 64f2a05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T20:23:01+01:00 Download 9aacf44
Download f0bf033 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:35:22+01:00 Download 424e2bb
Download ccec071 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-01 02:49:48
Download a7df43c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-30T12:04:47+01:00
Download 85e0848 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-12-01T04:23:10+01:00

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

Trying to find witnesses for program (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0cc1590 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T01:28 CET (sv-comp)
Download 9babfb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 6 2018-12-08T05:26:51
Download 8ffa83b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 36 2018-12-07T14:30 CET (sv-comp)
Download d5e18d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 89 2018-12-07T07:49:14+01:00
Download ffe04af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-10T20:37:22+01:00 Download df3a48e
Download e09694d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 125 2018-12-09T20:24:49+01:00 Download 836baee
Download 5b7b1fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-09T18:20:57+01:00 Download ce814fe
Download a8859a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-08T23:42:29+01:00 Download 0cc1590
Download 6f4899f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-08T22:09:35+01:00 Download 9babfb9
Download a194c1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-08T08:12:06+01:00 Download d5e18d0
Download 769ffb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-08T05:00:33+01:00 Download 26e8e1b
Download 4783794 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 111 2018-12-07T17:45:31+01:00 Download 8ffa83b
Download 0947916 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-06T10:20:04+01:00 Download 98fe76d
Download b61a53d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 90 2018-12-06T09:49:07+01:00 Download f626a90
Download 226c3ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 193 2018-12-06T09:10:59+01:00 Download 201abac
Download f626a90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 89 2018-12-05T14:23:51+01:00
Download b0feb9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:53:07+01:00 Download da87497
Download 7cc9e65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:36:02+01:00 Download 69dba66
Download 3d96ea9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:42:10+01:00 Download c45ef06
Download 4417192 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-07T22:59:07+01:00
Download 2680baa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:55:28+01:00
Download 8db911c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:49:03+01:00
Download a709ab4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-06T04:11:24+01:00

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

Trying to find witnesses for program (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1b12e88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-02T18:44 CET (sv-comp)
Download b7c2daa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 76 2017-12-02T18:28Z
Download c87fac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T07:28 CET (sv-comp)
Download 3c20dfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 76 2017-12-02T17:33Z
Download df85b1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T17:31:11.030648
Download 6fe0f5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:46:15.619189
Download 78676d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 9 2017-12-01T16:35 CET (sv-comp)
Download 8e6f6b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 9 2017-11-30T23:54 CET (sv-comp)
Download ccdf05b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 52 2017-11-30T13:49:35+01:00
Download b02a4c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 120 2017-11-30T21:58:50+01:00
Download 19d040c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 50 2017-12-01T00:59:40+01:00
Download 36c4e4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 71 2017-12-02T00:09:40+01:00
Download c94ed95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 66 2017-11-30T15:32 CET (sv-comp)
Download 50d3705 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 76 2017-12-02T14:58Z
Download 263214f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 40 2017-11-30T21:59 CET (sv-comp)
Download 66a7979 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T17:39:35+01:00
Download 48f5d9e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:13Z
Download 341325c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T16:58 CET (sv-comp)

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

Trying to find witnesses for program (954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b, sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c, 954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/954374a1ec67de60deabd487105719b48c8f2770febc2f12a7e9a031da3b9e3b.json

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