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/Problem03_label27_false-unreach-call.c
programSHA 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
witnessName results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.Problem03_label27_false-unreach-call.c.files/witness.graphml
witnessSHA 9d3ee3f7082146738a7fea27232b92e1071c0934cfa892f7b9f73e3bf6373599

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T00:05:25+01:00
producer CPAchecker 1.6.1-svn 26758M
program-sha256 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
programfile ../../sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c
programhash 4b0a0f778efa43429684de6acf0eda5b289d9868
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/9d3ee3f7082146738a7fea27232b92e1071c0934cfa892f7b9f73e3bf6373599.graphml
witness-sha256 9d3ee3f7082146738a7fea27232b92e1071c0934cfa892f7b9f73e3bf6373599
witness-size 832733
witness-type violation_witness

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

Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).

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

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

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

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

Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6353eb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 08:35:14
Download e4a663c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 117 2019-12-03T22:21 CET (comp)
Download 7d0ffb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 390 2019-12-11T21:41:19+01:00 Download 1370e65
Download 38494fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 390 2019-12-11T21:09:37+01:00 Download 6353eb1
Download f1bf77a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 390 2019-12-11T20:54:49+01:00 Download 872e57c
Download cf5aff9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 390 2019-12-11T20:44:30+01:00 Download 394b040
Download 8a0b3b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 391 2019-12-08T01:52:26+01:00 Download be52c73
Download 9c224db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 518 2019-12-04T02:58:19+01:00 Download e4a663c
Download 5173b8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 390 2019-12-03T08:08:51+01:00 Download aaae5e4
Download aaae5e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 390 2019-11-30T14:51:25+01:00
Download 1370e65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 390 2019-12-01T17:55:31+01:00
Download 6afa3dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 685 2019-12-07T21:14:13+01:00 Download 2321e4f

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

Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).

Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4de3834 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T10:10 CET (sv-comp)
Download acd413f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 11 2018-12-08T03:48:05
Download 8a9969f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 127 2018-12-07T10:34 CET (sv-comp)
Download 4abc341 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 394 2018-12-07T23:14:35+01:00
Download dfd7038 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 391 2018-12-10T20:38:02+01:00 Download 14be678
Download 4b84823 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-09T18:21:35+01:00 Download 5548683
Download 87b8475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 393 2018-12-08T23:44:07+01:00 Download 4de3834
Download d435a22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-08T22:10:35+01:00 Download acd413f
Download 222e3d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-08T08:05:17+01:00 Download 4abc341
Download 210e882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-08T05:01:49+01:00 Download b3e6422
Download 965ff6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 518 2018-12-07T17:43:18+01:00 Download 8a9969f
Download 92a0f3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-06T10:18:13+01:00 Download c6d1c55
Download ba76f22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-06T09:48:55+01:00 Download 4955ba3
Download ef08a78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 518 2018-12-06T09:20:07+01:00 Download 830ddba
Download 4955ba3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-06T05:04:45+01:00
Download ade1af7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 685 2018-12-09T20:54:34+01:00 Download e1c5b6e

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

Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).

Found 9 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5762904 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-02T22:55 CET (sv-comp)
Download 8b0f477 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T06:13 CET (sv-comp)
Download 18adfe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T12:40:42.702609
Download 3c5389b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T12:04:06.452187
Download 14a0381 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 19 2017-12-01T00:32 CET (sv-comp)
Download 381b08e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 223 2017-11-30T18:00:55+01:00
Download 9d3ee3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 833 2017-12-01T00:05:25+01:00
Download 1bc95fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 144 2017-11-30T12:23 CET (sv-comp)
Download ab12923 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 145 2017-11-30T19:08 CET (sv-comp)

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

Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).

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

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