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_label29_true-unreach-call_false-termination.c
programSHA a8f0f1e3c30f3f4c6057a5bcfa5d9b8d209be1f6e3ff6cf8b7dadc7969638cb8
witnessName results-verified/aprove.2018-12-04_2241.logfiles/sv-comp19_prop-termination.Problem02_label29_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 0f5a1bb81538d84ac7ce21ff5313f343399a4a49c1fb0c52c1d3ef3b0617b359

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2018-12-05T01:44 CET (sv-comp)
producer AProVE
programfile /tmp/vcloud-vcloud-master/worker/working_dir_38cc0adc-31a4-4a11-9033-b1934ca3b0c9/sv-benchmarks/c/eca-rers2012/Problem02_label29_true-unreach-call_false-termination.c
programhash 9B698DCF3C9DF7B9AD57A5812BD690B0917B122E
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/0f5a1bb81538d84ac7ce21ff5313f343399a4a49c1fb0c52c1d3ef3b0617b359.graphml
witness-sha256 0f5a1bb81538d84ac7ce21ff5313f343399a4a49c1fb0c52c1d3ef3b0617b359
witness-size 3768
witness-type violation_witness

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

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

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label29_true-unreach-call_false-termination.c, a8f0f1e3c30f3f4c6057a5bcfa5d9b8d209be1f6e3ff6cf8b7dadc7969638cb8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a8f0f1e3c30f3f4c6057a5bcfa5d9b8d209be1f6e3ff6cf8b7dadc7969638cb8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 109da85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:22:10+01:00 Download cbe2639
Download 75aeb86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:08:53+01:00 Download 55e1566
Download a9e8730 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:03:11+01:00 Download d2d7029
Download b11e9f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-08T00:42:45+01:00 Download 05dddca
Download 7561f25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T23:42:28+01:00 Download 4497997
Download 49c4c3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T19:46:52+01:00 Download 7dea2f8
Download 93f7ee9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:03:05+01:00 Download e68aa0e
Download 2c282f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-11-30T17:00:43+01:00 Download 7c0d43c
Download 7c0d43c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 280 2019-11-29T16:37:29+01:00
Download 55e1566 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 280 2019-12-01T01:43:44+01:00
Download 4263d0d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-01 01:52:17
Download 3c45591 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-30T06:53:15+01:00
Download 383465a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-11-30T23:45:08+01:00

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

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

Found 17 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label29_true-unreach-call_false-termination.c, a8f0f1e3c30f3f4c6057a5bcfa5d9b8d209be1f6e3ff6cf8b7dadc7969638cb8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a8f0f1e3c30f3f4c6057a5bcfa5d9b8d209be1f6e3ff6cf8b7dadc7969638cb8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b417bc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T19:36:12
Download bc655c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 280 2018-12-07T12:15:13+01:00
Download 2a6113a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-10T20:10:28+01:00 Download c0050f9
Download e7584b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:35:03+01:00 Download 61f466e
Download cdd8014 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:09:06+01:00 Download 8e81cee
Download 56bac9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T19:55:52+01:00 Download 733e3a3
Download 2fde92b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T21:30:31+01:00 Download b417bc7
Download e6065b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T06:36:52+01:00 Download bc655c7
Download a86eb00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T03:24:36+01:00 Download 417971e
Download 6988edb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:28:26+01:00 Download 5b09baa
Download 21b1f73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:10:50+01:00 Download 46ad580
Download e568258 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T07:41:42+01:00 Download d5e9c07
Download 46ad580 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-05T20:29:39+01:00
Download 9ec47cd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-06T13:21:52+01:00
Download ebfe4f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:37:33+01:00
Download c1b3e43 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:48:55+01:00
Download 8feb131 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-06T02:36:55+01:00

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

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

Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label29_true-unreach-call_false-termination.c, a8f0f1e3c30f3f4c6057a5bcfa5d9b8d209be1f6e3ff6cf8b7dadc7969638cb8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a8f0f1e3c30f3f4c6057a5bcfa5d9b8d209be1f6e3ff6cf8b7dadc7969638cb8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 014bc79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 183 2017-12-02T06:20Z
Download 5d9fb5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download ec66d3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T04:21:55+01:00 ad1d7d6
Download 5f6e648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 289 2017-12-03T02:03:50+01:00 33f8ca9
Download 4306519 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T01:36:51+01:00 8214acf
Download c8dd98a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-02T14:25:59+01:00 97f31e6
Download 5048004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:24:42+01:00 a683035
Download f51081f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:08:02+01:00 dfdec11
Download 05aeeb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:05:28+01:00 0858ced
Download e5cde90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:57:06+01:00 0e3d840
Download e2f4923 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T02:28:13+01:00
Download bfce3b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 319 2017-12-01T01:25:17+01:00
Download 32e491a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 280 2017-11-30T14:10:34+01:00
Download 8cadbaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 469 2017-12-02T13:08:13+01:00
Download 0910893 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 161 2017-12-02T13:12Z
Download bc15e10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 811 2017-11-30T15:26 CET (sv-comp)
Download a3d69dc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T13:03:29+01:00
Download b80b363 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:17Z
Download 79e928a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T16:14 CET (sv-comp)

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

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

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

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