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_label52_true-unreach-call_false-termination.c
programSHA 2c35e9af5f326bd7e9759765769fd7decbe3aec48ae39240eb898f3d6f0a76c4
witnessName results-verified/uautomizer.2017-12-03_1212.logfiles/sv-comp18.Problem02_label52_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA b73121857a15a4b2cdb4a3916ebdb3650b296327cc76a90c5eda75063f3c314d

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/b73121857a15a4b2cdb4a3916ebdb3650b296327cc76a90c5eda75063f3c314d.json

Key Value
architecture 32bit
creationtime 2017-12-03T11:18Z
producer Automizer
program-sha256 2c35e9af5f326bd7e9759765769fd7decbe3aec48ae39240eb898f3d6f0a76c4
programfile /tmp/vcloud-vcloud-master/worker/working_dir_b2c0d15c-efb6-49f4-865d-fc08c7b676d0/sv-benchmarks/c/eca-rers2012/Problem02_label52_true-unreach-call_false-termination.c
programhash b953cc2449a7f939fba62b70833772464a0d90fd
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/b73121857a15a4b2cdb4a3916ebdb3650b296327cc76a90c5eda75063f3c314d.graphml
witness-sha256 b73121857a15a4b2cdb4a3916ebdb3650b296327cc76a90c5eda75063f3c314d
witness-size 15163
witness-type violation_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d830c73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:18:27+01:00 Download 10406e5
Download 69c0e0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:17:44+01:00 Download 114ce43
Download 5a6820f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:02:32+01:00 Download d579c52
Download ae50c57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-08T00:57:40+01:00 Download 39dbf3f
Download 18e4f2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T23:28:36+01:00 Download 085f2de
Download a8abf85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T19:45:36+01:00 Download f0704b3
Download 0215a39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:03:08+01:00 Download 5f805aa
Download fe95414 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-11-30T16:15:19+01:00 Download 163e793
Download 163e793 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 280 2019-11-30T04:49:48+01:00
Download 10406e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 280 2019-12-01T08:04:19+01:00
Download be130be Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-02 02:36:16
Download 33be19f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-29T21:52:55+01:00
Download 51397ea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-11-30T20:42:19+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e018c4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T11:45:47
Download e8a4448 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 280 2018-12-07T01:40:40+01:00
Download f380b21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-10T20:03:55+01:00 Download 8ba09c0
Download 699ed9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:21:47+01:00 Download 01e28b8
Download e439779 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T19:48:13+01:00 Download df889f7
Download 75049b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T17:18:01+01:00 Download a675b9b
Download e73e643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T21:29:32+01:00 Download e018c4f
Download cb9da22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T06:35:38+01:00 Download e8a4448
Download 38d4790 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T04:16:32+01:00 Download 63a6d8c
Download 4d8c4f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:28:23+01:00 Download 0df1a03
Download c36a749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:00:14+01:00 Download 4513c28
Download b2f9834 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T07:59:39+01:00 Download 969f5b1
Download 4513c28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-05T17:40:54+01:00
Download 10de6a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-06T13:17:07+01:00
Download 67ad07c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:54:47+01:00
Download 4686894 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:48:50+01:00
Download ead7ba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-05T06:20:34+01:00

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

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

Found 21 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label52_true-unreach-call_false-termination.c, 2c35e9af5f326bd7e9759765769fd7decbe3aec48ae39240eb898f3d6f0a76c4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2c35e9af5f326bd7e9759765769fd7decbe3aec48ae39240eb898f3d6f0a76c4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7219e02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 161 2017-12-03T00:34Z
Download c2aca79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 178 2017-12-02T20:31Z
Download 13d7bfa 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 bc62577 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T06:50:52+01:00 d1d4fbf
Download 1f0f3e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T04:27:40+01:00 6d65a8d
Download eb6573d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T01:59:12+01:00 5b4ec1b
Download 98a2fe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T00:58:53+01:00 1f8e063
Download 0494220 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-02T15:09:37+01:00 cf0cd29
Download e49ec18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:46:06+01:00 3a9b3c5
Download 53e64c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:26:51+01:00 92f8e4f
Download f782976 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:07:47+01:00 1288f4a
Download 03f9cf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:34:07+01:00 4cbd36d
Download cce1601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-11-30T17:40:54+01:00
Download 645dcc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 337 2017-11-30T23:59:42+01:00
Download f1f75b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 280 2017-11-30T22:36:19+01:00
Download 7741221 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 411 2017-12-01T23:58:13+01:00
Download c2ca65a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 161 2017-12-02T03:45Z
Download 3f7344a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 811 2017-11-30T13:36 CET (sv-comp)
Download 1552d1b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T15:53:58+01:00
Download b731218 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:18Z
Download 0e7a7fd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T16:24 CET (sv-comp)

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

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

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

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