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/eca-rers2012/Problem06_label10_false-unreach-call.c
programSHA f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.Problem06_label10_false-unreach-call.c.files/witness.graphml
witnessSHA e5037cea1a85ce77ab1bf2b88e9790172b93b03a332c07febdbc3b9d77230c03

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T16:53:25+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
programfile ../../sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c
programhash f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e5037cea1a85ce77ab1bf2b88e9790172b93b03a332c07febdbc3b9d77230c03.graphml
witness-sha256 e5037cea1a85ce77ab1bf2b88e9790172b93b03a332c07febdbc3b9d77230c03
witness-size 2106413
witness-type violation_witness

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

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

Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 10 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8436c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 14:43:15
Download fbb19de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 589 2019-12-04T00:15 CET (comp)
Download 5b87264 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2067 2019-12-11T21:40:19+01:00 Download 0d66b59
Download 12509c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2066 2019-12-11T21:09:35+01:00 Download 8436c9c
Download c4efe82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2067 2019-12-11T20:54:34+01:00 Download e9c2b90
Download 8a1bfe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2067 2019-12-11T20:44:39+01:00 Download 8eee1c7
Download c5035be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2768 2019-12-04T02:58:26+01:00 Download fbb19de
Download 73d25b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2067 2019-12-03T08:01:32+01:00 Download 3f467e7
Download 3f467e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 2106 2019-11-29T21:37:15+01:00
Download 0d66b59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 2094 2019-11-30T23:20:05+01:00

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

Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 898afc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T11:13 CET (sv-comp)
Download 58f4f46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 639 2018-12-07T06:37 CET (sv-comp)
Download e5037ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 2106 2018-12-07T16:53:25+01:00
Download ce662f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2067 2018-12-09T18:22:01+01:00 Download 4ed07c0
Download f4da48b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2067 2018-12-08T08:42:54+01:00 Download e5037ce
Download 2e00bef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2066 2018-12-08T05:04:34+01:00 Download 98f6d6a
Download e8e99c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2768 2018-12-07T17:45:55+01:00 Download 58f4f46
Download 5c5ce5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2067 2018-12-06T10:09:48+01:00 Download 75e0bc5
Download 1963708 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2067 2018-12-06T09:48:54+01:00 Download 68efadd
Download 269f301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2770 2018-12-06T09:15:11+01:00 Download 1d2b0c6
Download 68efadd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2106 2018-12-06T04:51:56+01:00

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

Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae17af2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:13 CET (sv-comp)
Download 69b33f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T02:23:05.790027
Download 52071b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T16:23:44.707837
Download ec49949 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 1166 2017-11-30T18:09:08+01:00
Download ded981c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 731 2017-11-30T11:52 CET (sv-comp)

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

Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json

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