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/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c
programSHA 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
witnessName results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml
witnessSHA a633f6c54fe75b6d32d6c4ca1a7fa702f32dff62eca2ec80081b454375652185

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T00:04 CET (sv-comp)
producer Symbiotic
program-sha256 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
programfile /tmp/vcloud-vcloud-master/worker/working_dir_ee41e6eb-a5db-46d2-bd7f-c93f5deb013a/sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c
programhash ccd6d122756047ddb1225c106ac06a6748e14c22
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a633f6c54fe75b6d32d6c4ca1a7fa702f32dff62eca2ec80081b454375652185.graphml
witness-sha256 a633f6c54fe75b6d32d6c4ca1a7fa702f32dff62eca2ec80081b454375652185
witness-size 777
witness-type correctness_witness

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

Trying to find witnesses for program (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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 (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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 (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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 (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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 (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 15 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 40273a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 15 2019-11-29T17:12:28+01:00
Download b903787 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 15 2019-11-30T21:14:49+01:00
Download 182fc8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-12-11T20:22:37+01:00 Download 49a6e9c
Download 0a7eea2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-12-11T20:17:28+01:00 Download a023968
Download e28cc75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-12-11T20:02:18+01:00 Download 2069709
Download eb8c1fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-12-08T00:39:58+01:00 Download a637597
Download 1c59f39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-12-07T23:45:29+01:00 Download 9b7f621
Download a8df326 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-12-07T19:45:37+01:00 Download 5b69b63
Download 1818005 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-12-05T19:02:50+01:00 Download 2606d84
Download b3149bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 15 2019-11-30T17:14:28+01:00 Download 0aa04b7
Download 0aa04b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 15 2019-11-30T02:34:53+01:00
Download a637597 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 15 2019-12-07T14:35:13+01:00
Download a023968 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 15 2019-11-30T22:54:35+01:00
Download d2101fe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 25 2019-11-29T16:45:41+01:00
Download b571bdb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 25 2019-12-01T00:00:59+01:00

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

Trying to find witnesses for program (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 23 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fd3d6dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T08:34 CET (sv-comp)
Download 2b181f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-05T15:47:02+01:00
Download 204fa53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 15 2018-12-08T03:17:33+01:00
Download 04a8135 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T10:39 CET (sv-comp)
Download a10c749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T16:43:46
Download b63c782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 15 2018-12-06T21:25:40+01:00
Download 2d1428b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-10T20:08:05+01:00 Download 068ad9b
Download d6d3612 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-09T20:14:31+01:00 Download cd43580
Download bac139a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-09T19:53:00+01:00 Download 3c9c1b4
Download c278f92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-09T17:13:06+01:00 Download 9a25083
Download 111f514 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-08T23:09:47+01:00 Download 04a8135
Download 6d796bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-08T21:38:22+01:00 Download a10c749
Download ca4e277 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-08T06:28:31+01:00 Download b63c782
Download a0ff806 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-08T03:48:08+01:00 Download 064913a
Download 87c6652 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-07T17:45:12+01:00 Download bb0db58
Download 80b2bad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-06T09:28:47+01:00 Download 281ecb4
Download 7497dec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-06T08:52:31+01:00 Download 5baebe2
Download 5baebe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-06T07:49:51+01:00
Download 1b5a919 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-06T07:41:48+01:00 Download 1766138
Download 4bc2d9d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 25 2018-12-07T05:53:41+01:00
Download d823ff0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-09T20:34:31+01:00
Download dfce4f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-06T09:41:41+01:00
Download 0fffcdb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-06T07:49:15+01:00

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

Trying to find witnesses for program (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 37 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 96f88a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-03T00:19 CET (sv-comp)
Download ff9e5a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T11:13:02.365524
Download 1570c8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 3.1 33 2017-12-01T09:16 CET (sv-comp)
Download 30e3fd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 22 2017-12-03T06:53Z
Download 1b048e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 23 2017-12-03T04:07Z
Download f84eae7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 22 2017-12-03T03:43Z
Download da2096b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 34 2017-12-01T08:21 CET (sv-comp)
Download bb0db58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:26 CET (sv-comp)
Download 5a6e192 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 22 2017-12-03T02:39Z
Download a633f6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T00:04 CET (sv-comp)
Download 1a6355b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 23 2017-12-02T12:50Z
Download 9cf329a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T19:45:58.248002
Download ee1be48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 33 2017-12-01T17:11 CET (sv-comp)
Download dc93d52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 15 2017-12-02T21:20:35+01:00
Download 8c0bc5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T17:40:39+01:00
Download 093f187 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-03T07:03:54+01:00 fb1f688
Download 5f3b758 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-03T04:26:21+01:00 7764d1d
Download f7c5956 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-03T02:35:04+01:00 4e9687b
Download 4c63d50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-03T01:54:49+01:00 a11034a
Download 49f458c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-02T20:09:10+01:00 4ae75f3
Download c140b6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-02T14:49:53+01:00 0582873
Download 19141b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-02T08:37:06+01:00 217aab7
Download 37316ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-02T00:09:03+01:00 9ba1390
Download bec8121 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-01T08:13:56+01:00 bddf76b
Download 2fc21d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-01T06:23:08+01:00 f4b33a1
Download a2ffb61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-01T05:39:11+01:00 ef6a8d0
Download 9466a0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-01T04:55:44+01:00 2efec5c
Download 161fee2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-01T04:35:11+01:00 05298f3
Download 883f70a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 15 2017-12-01T01:59:14+01:00
Download 7a89b67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 16 2017-12-01T00:18:32+01:00
Download f695dd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 15 2017-11-30T17:58:04+01:00
Download a15f96e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 14 2017-12-01T19:12:35+01:00
Download 61c645a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 22 2017-12-02T04:59Z
Download d12da80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 34 2017-11-30T11:41 CET (sv-comp)
Download d1f1df8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 25 2017-12-01T14:43:59+01:00
Download ecb4982 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 18 2017-12-03T11:12Z
Download a78ac71 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 15 2017-12-01T13:50 CET (sv-comp)

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

Trying to find witnesses for program (960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa, sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json

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