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/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c
programSHA e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.s3_srvr_1_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA eff2ee5720194f7b8dd86b6dfe091efc1156f103e899a333d043c9cf1a6c664e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T17:21 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
programfile /tmp/vcloud-vcloud-master/worker/working_dir_6d2d48ec-6ddc-4df5-a830-a1d29491da13/sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c
programhash 28d8096126b63ab25306739ff4b0685d3f7b94a5
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/eff2ee5720194f7b8dd86b6dfe091efc1156f103e899a333d043c9cf1a6c664e.graphml
witness-sha256 eff2ee5720194f7b8dd86b6dfe091efc1156f103e899a333d043c9cf1a6c664e
witness-size 16598
witness-type violation_witness

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

Trying to find witnesses for program (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.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 (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.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 (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.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 (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.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 (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.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 (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 22 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ce7866b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T09:09 CET (sv-comp)
Download ac7ba96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 11 2018-12-08T02:15:00
Download 7bddba0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 58 2018-12-07T12:12 CET (sv-comp)
Download ebeb3c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 73 2018-12-10T17:42:40+01:00
Download 9994c6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 75 2018-12-07T08:55:28+01:00
Download d14ea35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 83 2018-12-10T20:38:11+01:00 Download ebeb3c3
Download f512f64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 83 2018-12-09T20:53:21+01:00 Download 17298ee
Download 50cf0db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 83 2018-12-09T20:40:04+01:00 Download 3d73aa8
Download 7a68c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 84 2018-12-09T20:34:07+01:00 Download b5709bd
Download 2d10e32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 84 2018-12-09T18:19:08+01:00 Download 3d65623
Download 6c5790f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 83 2018-12-08T23:43:22+01:00 Download ce7866b
Download c2c3f8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 84 2018-12-08T22:08:36+01:00 Download ac7ba96
Download f7b8bf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 83 2018-12-08T08:10:50+01:00 Download 9994c6c
Download 35c1781 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 84 2018-12-08T05:04:33+01:00 Download 0e54da9
Download 93ae1c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 97 2018-12-07T17:11:08+01:00 Download 7bddba0
Download 2059f5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 84 2018-12-07T01:18:28+01:00 Download 0d49675
Download 7eba603 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 84 2018-12-06T10:18:34+01:00 Download ca8dca1
Download 988df2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 83 2018-12-06T09:49:17+01:00 Download 724062a
Download 9bf4b43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 97 2018-12-06T09:17:27+01:00 Download b33c7de
Download 724062a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 74 2018-12-05T20:38:41+01:00
Download f2533c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 54 2018-12-06T09:42:07+01:00 Download 9b1042b
Download b8b97c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 54 2018-12-06T09:09:40+01:00 Download d1a4254

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

Trying to find witnesses for program (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 18 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b4ec6da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 85 2017-12-03T02:44Z
Download 87ac71e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T03:07 CET (sv-comp)
Download b2d4ae8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 86 2017-12-02T19:55Z
Download 3a928cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 8 2017-12-01T14:31:19.648598
Download f6d344d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 9 2017-12-01T11:01:54.177682
Download 1beede7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 17 2017-12-01T19:33 CET (sv-comp)
Download eff2ee5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 17 2017-11-30T17:21 CET (sv-comp)
Download a2f447a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 73 2017-12-02T22:07:48+01:00
Download 51e1153 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 64 2017-12-01T02:40:22+01:00
Download 918ec8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 94 2017-11-30T17:51:57+01:00
Download d770b09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 56 2017-12-01T02:18:48+01:00
Download f7e7b90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 36 2017-12-02T13:09:31+01:00
Download 75f64dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 62 2017-11-30T11:50 CET (sv-comp)
Download 5489ed5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 85 2017-12-02T05:43Z
Download dd8281a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 54 2017-12-01T02:41 CET (sv-comp)
Download 0daed8d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 139 2017-12-01T14:36:21+01:00
Download a0881c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 126 2017-12-03T11:18Z
Download ebead82 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 100 2017-12-01T12:40 CET (sv-comp)

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

Trying to find witnesses for program (e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305, sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c, e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e0412718bede801ea57bba33a3daec1ba8a69fa30ea24196ce6d895672be1305.json

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