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/recursive-simple/sum_20x0_true-unreach-call_true-termination.c
programSHA a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
witnessName results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.sum_20x0_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 4152da641763c657d62d47b73c39c898706819d4734252e950ed5f9a1e4d25d0

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-03T03:09Z
producer Taipan
program-sha256 a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
programfile /tmp/vcloud-vcloud-master/worker/working_dir_943a4daf-3f81-4b66-9f72-242a4c9e6e55/sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c
programhash f4078ef7bc39da0337b6d8ed5ecbbcec336a37b8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/4152da641763c657d62d47b73c39c898706819d4734252e950ed5f9a1e4d25d0.graphml
witness-sha256 4152da641763c657d62d47b73c39c898706819d4734252e950ed5f9a1e4d25d0
witness-size 6224
witness-type correctness_witness

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

Trying to find witnesses for program (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.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 (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.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 (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.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 (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.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 (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 15 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 36597d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:03 CET (comp)
Download 0464d4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:29:01+01:00 Download b1cdcc4
Download f04eff1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:13:34+01:00 Download 2e23234
Download 6373999 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:02:47+01:00 Download 39b5ac7
Download 9945844 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:53:03+01:00 Download edb219a
Download 8dbd898 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:44:10+01:00 Download 808816d
Download d564c20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T19:45:33+01:00 Download 0d62233
Download 85c5dc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:00:03+01:00 Download 172bf26
Download b4ba5f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:13:14+01:00 Download b47f5ce
Download a57057a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:07:34+01:00 Download 36597d1
Download 0818f38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T19:57:09+01:00 Download 1f53560
Download 6b966dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T16:59:10+01:00 Download 66173b6
Download 66173b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 5 2019-11-29T16:17:34+01:00
Download 2e23234 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T01:38:37+01:00
Download 01d247f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T21:48 CET (comp)

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

Trying to find witnesses for program (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 22 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 139f9af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T12:10 CET (sv-comp)
Download 0dfc22c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:46:54
Download d2c1595 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T20:53 CET (sv-comp)
Download f9457b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-06T21:16:26+01:00
Download fb0ed64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T19:52:42+01:00 Download 671ee77
Download 427bb1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:12+01:00 Download 752dceb
Download 96d742b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T21:06:29+01:00 Download 1d70cfe
Download 098bf61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:20:31+01:00 Download b2ca64e
Download 8a5e22b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:17:42+01:00 Download e799f4f
Download d4dceef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:48:19+01:00 Download 139f9af
Download 93b20bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:40:55+01:00 Download 0dfc22c
Download 5d42957 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:46:50+01:00 Download f9457b6
Download c2a79cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:51:05+01:00 Download 5ef3440
Download 0fc9878 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T01:48:51+01:00 Download 752dceb
Download 1dcc94a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:43:25+01:00 Download 4104342
Download db18e36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:38:27+01:00 Download d2c1595
Download 6229593 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:19+01:00 Download f551cfb
Download ad10f43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:03:11+01:00 Download 3349de0
Download d7d4cbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:59:59+01:00 Download c33bfe9
Download 3349de0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T12:41:05+01:00
Download 47d0cf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T09:35 CET (sv-comp)
Download bb5af0e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T11:22 CET (sv-comp)

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

Trying to find witnesses for program (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 29 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bf59abf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T11:40:19+01:00
Download 6b8b3fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T01:20:32+01:00
Download 97d087f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T07:43:41+01:00
Download 4104342 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:00 CET (sv-comp)
Download 4152da6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-03T03:09Z
Download 5b415e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T11:08 CET (sv-comp)
Download 8d0cc75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T20:16 CET (sv-comp)
Download 26020e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:13:33.824095
Download 1ecbc5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:35:50.364029
Download 831c06c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T18:12:10.588026
Download 9888408 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:21:48.548763
Download db5064c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T17:08 CET (sv-comp)
Download ecb2200 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 0dfdfeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-11-30T17:56:12+01:00
Download 1896b2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T06:59:30+01:00 d081b0a
Download 4100eb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:06:53+01:00 96fab08
Download 050cf0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:48:08+01:00 1482589
Download f50d7ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:08:07+01:00 c180096
Download c411aa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T07:59:07+01:00 633b9b9
Download 9f7370a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:11:47+01:00 0543dec
Download 17f4e09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:24:36+01:00 77274a4
Download f1ede12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:06:08+01:00 83608ca
Download e2ec6d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:33+01:00 5eaa639
Download a945006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:05:08+01:00 c20980f
Download 8c31fda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:34:14+01:00 d68f1b1
Download 57c5b60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T13:12:24+01:00
Download 0710480 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 16 2017-11-30T12:26 CET (sv-comp)
Download c309571 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T14:49Z
Download 17df3be Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 16 2017-12-01T15:31 CET (sv-comp)

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

Trying to find witnesses for program (a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a, sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_20x0_true-unreach-call_true-termination.c, a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a72ad859cde47c251089bdee1e87120e828531496eae3ecfe80a55d6a2ebc17a.json

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