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/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i
programSHA df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
witnessName results-validated/cpa-seq-validate-violation-witnesses-map2check.2018-12-07_0102.logfiles/sv-comp19_prop-reachsafety.verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 54a82b15c7d79ce8d951b8cd4c2589de251eacc7e681041e6b3b1d32055d408a

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/54a82b15c7d79ce8d951b8cd4c2589de251eacc7e681041e6b3b1d32055d408a.json

Key Value
architecture 32bit
creationtime 2018-12-07T01:22:43+01:00
inputwitnesshash 76547eab7ac38cbb770faee1f90ad19582ecd889aeb90901664bf0e1fbc24f51
producer CPAchecker 1.7-svn 29852
program-sha256 df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
programfile ../../sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i
programhash df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/54a82b15c7d79ce8d951b8cd4c2589de251eacc7e681041e6b3b1d32055d408a.graphml
witness-sha256 54a82b15c7d79ce8d951b8cd4c2589de251eacc7e681041e6b3b1d32055d408a
witness-size 7034
witness-type correctness_witness

This witness was created for this program (cf. table above, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c).

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

Trying to find witnesses for program (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.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 (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.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 (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.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 (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.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 (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.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 '19

Trying to find witnesses for program (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 24 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d5c9776 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T07:48 CET (sv-comp)
Download a446a99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 13 2018-12-08T19:04:47
Download 9d1bfb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 31 2018-12-07T10:04 CET (sv-comp)
Download 12dd51f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 39 2018-12-07T23:50:44+01:00
Download 3616a58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 42 2018-12-09T20:53:21+01:00 Download cdf85c5
Download fff939e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 42 2018-12-09T20:36:39+01:00 Download 3031c2f
Download 09b42f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T22:09:37+01:00 Download a446a99
Download 776187a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T08:59:59+01:00 Download 12dd51f
Download b91fa3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-08T05:01:49+01:00 Download 370f437
Download 1dc78d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 42 2018-12-07T17:26:08+01:00 Download 9d1bfb3
Download 4e92abc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-06T10:18:28+01:00 Download d779c31
Download 1600b8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-06T09:48:11+01:00 Download 0ffe84c
Download f8b99b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 42 2018-12-06T09:17:06+01:00 Download 0327107
Download 0ffe84c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 39 2018-12-05T18:36:49+01:00
Download f4a819a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:35:21+01:00 Download f5de278
Download b50dff2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T18:23:15+01:00 Download 396f414
Download d3b3e0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:45:15+01:00 Download d5c9776
Download 5d3495d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T04:37:28+01:00 Download 1bf53a3
Download 347e059 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T18:47:54+01:00 Download 9f1fb10
Download 54a82b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:22:43+01:00 Download 76547ea
Download ea173b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:41:18+01:00 Download 85aa282
Download 269de65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:03:30+01:00 Download b62252e
Download 6e0206e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:07 CET (sv-comp)
Download b8efcea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T06:34 CET (sv-comp)

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

Trying to find witnesses for program (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 23 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 78f0d3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 7 2017-12-01T23:41 CET (sv-comp)
Download e623918 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 33 Sun Dec 3 02:02:32 2017
Download 26cc702 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 39 2017-12-03T02:58Z
Download 4b9f862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T05:06 CET (sv-comp)
Download ee41acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 12 2017-12-01T23:38:20.597579
Download 1843140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 12 2017-12-01T18:08:40.218202
Download 888f614 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-12-01T19:31 CET (sv-comp)
Download 39015a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-12-01T04:10 CET (sv-comp)
Download 6c05ba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 37 2017-12-01T03:52:16+01:00
Download 5efe299 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 35 2017-11-30T21:48 CET (sv-comp)
Download 5bdc6b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 38 2017-12-02T19:19Z
Download 4f428d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 33 2017-11-30T13:18 CET (sv-comp)
Download 6b38d76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T20:59 CET (sv-comp)
Download c89c43d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:03:13.354927
Download 46faa9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:54:06.270296
Download 7a03371 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T15:55:25+01:00 5a354a8
Download cdc6a47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:37:02+01:00 17cf5bd
Download fe61559 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T07:41:40+01:00 bfe6637
Download b249f00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T07:39:27+01:00 9df3b6d
Download 64670f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 14 2017-11-30T19:02:14+01:00
Download 7d72d2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T17:20:20+01:00
Download 7a9572b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 6 2017-12-02T00:20:06+01:00
Download 6100dea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 36 2017-12-01T19:24 CET (sv-comp)

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

Trying to find witnesses for program (df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c, sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i, df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/df33a606ed8dff6e0cd458b6a2a86f46509c229534b5b2e3fec472f3ad3ab62c.json

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