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/ldv-regression/test24_false-unreach-call.c
programSHA 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
witnessName results-verified/uautomizer.2018-12-08_0742.logfiles/sv-comp19_prop-reachsafety.test24_false-unreach-call.c.files/witness.graphml
witnessSHA 58e3b5c8a41b829568038867f9ca4e588fc75a936edc91787bfa42fb12c4faa2

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T14:48Z
producer Automizer
programfile /tmp/vcloud-vcloud-master/worker/working_dir_dff4d4c3-f374-438d-a077-1d6d5233827e/sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c
programhash 45294379b83c6b60e0b0199955cdf7244f057430
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/58e3b5c8a41b829568038867f9ca4e588fc75a936edc91787bfa42fb12c4faa2.graphml
witness-sha256 58e3b5c8a41b829568038867f9ca4e588fc75a936edc91787bfa42fb12c4faa2
witness-size 29852
witness-type violation_witness

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

Trying to find witnesses for program (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.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 (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.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 (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.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 (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.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 (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 18 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f4e3fcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 9 2019-12-01 20:49:50
Download e65c523 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 25 2019-12-04T00:30 CET (comp)
Download eca720a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-11T21:55:11+01:00 Download f5a18bc
Download 7449142 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-11T21:50:19+01:00 Download 44f4e5a
Download a795a83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-11T21:09:38+01:00 Download f4e3fcc
Download 3910de5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-11T20:44:34+01:00 Download cca23e4
Download 54c5e6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-08T01:51:18+01:00 Download f23ef19
Download af093d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-08T00:26:04+01:00 Download 6d07e7f
Download 21ee8e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-08T00:06:16+01:00 Download 08d85f8
Download f48b2b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-07T21:17:23+01:00 Download 8a404c7
Download 45dd153 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-04T02:58:23+01:00 Download e65c523
Download 6076e14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-03T08:56:50+01:00 Download d026346
Download 1cb8bb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 30 2019-12-03T08:08:47+01:00 Download 534691c
Download 534691c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 25 2019-11-30T05:32:01+01:00
Download f23ef19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 30 2019-12-07T15:29:43+01:00
Download 44f4e5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 25 2019-11-30T23:28:49+01:00
Download c738740 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-06T02:39:03+01:00 Download 78181b3
Download f94d4b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T20:20:31+01:00 Download de531a8

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

Trying to find witnesses for program (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 20 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download af67fe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T17:47 CET (sv-comp)
Download 13f58b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T11:26:48
Download 10b28d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 24 2018-12-10T18:54:31+01:00
Download e122cd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 25 2018-12-07T10:07:18+01:00
Download 1d6ac5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-10T20:35:11+01:00 Download 10b28d0
Download e372a01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-09T20:53:26+01:00 Download 8c6f9cc
Download 8361f5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-09T20:34:31+01:00 Download 58e3b5c
Download c6e9aab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-09T20:20:30+01:00 Download 0fcfeff
Download aa5dc06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-09T18:21:41+01:00 Download f3a4ddd
Download c5646e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-08T23:42:34+01:00 Download af67fe8
Download b907967 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-08T08:09:23+01:00 Download e122cd2
Download 02887c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-08T04:24:17+01:00 Download 19ef6a2
Download 6728451 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-07T18:47:44+01:00 Download b272ac4
Download 12c3d01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-07T09:23:07+01:00 Download b4e90fe
Download bc7dde5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-06T09:48:10+01:00 Download fe1b41b
Download 6b6cc5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 32 2018-12-06T09:06:29+01:00 Download 28283a1
Download fe1b41b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-05T22:44:49+01:00
Download f2d8b4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T22:07:30+01:00 Download 13f58b7
Download 61cea44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T10:18:25+01:00 Download 63bd806
Download 035abca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:03:35+01:00 Download f579535

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

Trying to find witnesses for program (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 11 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8118458 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 31 2017-12-03T01:22Z
Download 0ae2af0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T06:34 CET (sv-comp)
Download 2ae1140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 13 2017-12-01T19:51 CET (sv-comp)
Download 49b4408 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 29 2017-12-02T12:16Z
Download d427b09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 9 2017-12-01T04:17 CET (sv-comp)
Download 028c0b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 23 2017-11-30T15:31:22+01:00
Download 690626c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 41 2017-11-30T20:21:06+01:00
Download c80a456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 21 2017-11-30T20:33:28+01:00
Download b8f7624 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 18 2017-12-02T04:21:25+01:00
Download 42222d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 49 2017-11-30T22:28 CET (sv-comp)
Download 40888d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 29 2017-12-02T01:05Z

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

Trying to find witnesses for program (2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f, sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test24_false-unreach-call.c, 2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2ceb037cf4436f81b0904991cce72e4690c189f89ba8bb0a58ae0c3c74c9483f.json

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