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/volatile_alias_true-termination.c_true-unreach-call_1.i
programSHA e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
witnessName results-verified/forester.2017-12-01_1745.logfiles/sv-comp18.volatile_alias_true-termination.c_true-unreach-call_1.i.files/witness.graphml
witnessSHA c6364dcbfe55126cfbfec8607aafdf6e5bfe0e78ab0dbff44bdd5b4911d0a9db

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T18:09 CET (sv-comp)
memorymodel precise
producer Forester
program-sha256 e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
programfile ../../sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i
programhash 90b9159ba2a58602ff1e9c0acff32948b8aee8f8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c6364dcbfe55126cfbfec8607aafdf6e5bfe0e78ab0dbff44bdd5b4911d0a9db.graphml
witness-sha256 c6364dcbfe55126cfbfec8607aafdf6e5bfe0e78ab0dbff44bdd5b4911d0a9db
witness-size 3946
witness-type correctness_witness

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

Trying to find witnesses for program (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.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 (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.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 (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.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 (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.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 (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 19 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 050e7f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T01:26 CET (comp)
Download 77e03f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-11T20:29:10+01:00 Download 37f3bde
Download e9dc232 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-11T20:14:33+01:00 Download 79b3528
Download 976533b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-11T20:08:39+01:00 Download f870bcc
Download 3ee5be6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-11T20:02:17+01:00 Download cd3bcc5
Download fc4916a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-08T00:38:37+01:00 Download 2da0fe0
Download 64b2ad8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-07T23:46:06+01:00 Download 2f7c7bc
Download 43924d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-07T23:30:25+01:00 Download 20a89e8
Download 23688f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-07T19:43:54+01:00 Download c5a8a52
Download 9e05b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-06T02:06:55+01:00 Download bd8147b
Download 54aaca4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-05T19:12:50+01:00 Download bdc6a4a
Download ea18de4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-05T19:02:51+01:00 Download d605baa
Download 40c2dca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-12-04T02:07:29+01:00 Download 050e7f4
Download 69becc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-11-30T19:38:17+01:00 Download 5323370
Download f022ba8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 3 2019-11-30T17:07:27+01:00 Download 5a19d83
Download 5a19d83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 3 2019-11-30T00:57:32+01:00
Download 2da0fe0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 3 2019-12-07T16:34:27+01:00
Download f870bcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 3 2019-12-01T16:44:44+01:00
Download 181abbd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T21:46 CET (comp)

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

Trying to find witnesses for program (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 24 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 64f30a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T20:45 CET (sv-comp)
Download 35d826e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:47:03
Download 060c8aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T10:18 CET (sv-comp)
Download de267f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T01:44:56+01:00
Download c502844 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-10T19:56:54+01:00 Download 00cc3c6
Download acbe070 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:31:31+01:00 Download fab70ca
Download 19423a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:16:05+01:00 Download 0da703e
Download a0006b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:09:30+01:00 Download 4790cf0
Download 22c3534 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-09T19:54:45+01:00 Download 9a6244f
Download 2329ebf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:07:03+01:00 Download 64f30a8
Download 3c26ff1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T21:49:16+01:00 Download 35d826e
Download 73cdc00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T06:30:22+01:00 Download de267f1
Download 3028e4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T02:58:02+01:00 Download 2fb17b6
Download 8465dd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T02:00:36+01:00 Download fab70ca
Download 40196eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-07T17:44:46+01:00 Download 8befbbf
Download ca265a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-07T16:39:17+01:00 Download 060c8aa
Download b009d1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-07T08:03:04+01:00 Download 3276c9a
Download fb4979b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:28:56+01:00 Download 36b0439
Download 520d888 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:10:27+01:00 Download 749ac92
Download 0a17d39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T08:29:55+01:00 Download d8392d4
Download 749ac92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T07:58:27+01:00
Download 6781557 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T07:35:59+01:00 Download 5371ae2
Download aaf4f91 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:50 CET (sv-comp)
Download 68b508f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T00:36 CET (sv-comp)

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

Trying to find witnesses for program (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 41 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8befbbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:14 CET (sv-comp)
Download 26b97d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T00:51Z
Download 365eaf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T18:05 CET (sv-comp)
Download 3276c9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:54 CET (sv-comp)
Download e6433a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T21:08 CET (sv-comp)
Download 03b7ca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T17:41Z
Download c6364dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Forester 4 2017-12-01T18:09 CET (sv-comp)
Download 86b7d35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:09:50.909203
Download 9671457 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:47:10.258891
Download b7296a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T12:04:38.284422
Download 8abffaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T15:54:42.207787
Download 3e3cc1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T18:27 CET (sv-comp)
Download bca404c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 3 2017-12-02T21:32:02+01:00
Download 0c012d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T19:41:37+01:00
Download 657c0de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-03T07:06:07+01:00 d249f5c
Download c4f7a1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-03T04:29:47+01:00 01cc7b4
Download eb2a29c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-03T01:14:47+01:00 8bc0055
Download 362f3a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-02T23:45:52+01:00 1d9dfb6
Download 7863a4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-02T20:26:23+01:00 da09821
Download b41c94d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-02T14:21:11+01:00 102bc3f
Download 63c3030 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-02T08:27:58+01:00 dbf7b91
Download e8bd58c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-02T00:19:45+01:00 e44a87e
Download 21b9d36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T22:28:54+01:00 7954675
Download 6744335 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T22:13:54+01:00 5c98907
Download 4856d1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T21:03:53+01:00 2b29c12
Download 8aed82c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T18:33:50+01:00 b11f594
Download d7b98be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:13:47+01:00 7b9ab93
Download 93badfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T07:14:23+01:00 dd3e92d
Download 6fb348e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T06:53:22+01:00 11954f5
Download daf33c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T06:03:18+01:00 df92d76
Download 8a2c57b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T05:46:19+01:00 9c202df
Download bf6d41a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T05:12:30+01:00 1cdac69
Download f073c83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-11-30T18:33:47+01:00
Download a98088e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 7 2017-11-30T17:58:03+01:00
Download 0190a47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 3 2017-11-30T22:18:35+01:00
Download 341082d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-02T00:02:29+01:00
Download 82abcb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T14:40 CET (sv-comp)
Download f964df6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T18:57Z
Download 7d8a9ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-11-30T20:46 CET (sv-comp)
Download 454feba Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T15:36 CET (sv-comp)
Download 9032cdb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T16:31 CET (sv-comp)

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

Trying to find witnesses for program (e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca, sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i, e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e0f0c02e53aeeec8bef81ee2030fe1eea1bad780bf3f1361ce8d4497ac0761ca.json

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