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_label43_false-unreach-call.c
programSHA ff766465b4fb563e49220a7d767db6a205fa800df7586eb9629babc0a4694abd
witnessName results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.Problem03_label43_false-unreach-call.c.files/witness.graphml
witnessSHA b588a129e6fcc51142a6b336da8833e1e8f28d02cedbffcac32bf992cc0f76f4

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T16:19:34.320527
producer ESBMC 4.6.0 kind
program-sha256 ff766465b4fb563e49220a7d767db6a205fa800df7586eb9629babc0a4694abd
programfile ../../sv-benchmarks/c/eca-rers2012/Problem03_label43_false-unreach-call.c
programhash 2db0c11d814dfe1e3cc97b6314e8d585dfd00482
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b588a129e6fcc51142a6b336da8833e1e8f28d02cedbffcac32bf992cc0f76f4.graphml
witness-sha256 b588a129e6fcc51142a6b336da8833e1e8f28d02cedbffcac32bf992cc0f76f4
witness-size 4595
witness-type violation_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 32e2277 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 13:06:07
Download 4a4b515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 93 2019-12-03T22:48 CET (comp)
Download 6cf9517 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 295 2019-12-11T21:53:39+01:00 Download d9ee02b
Download 38b09b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 295 2019-12-11T21:09:07+01:00 Download 32e2277
Download 94ce2c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 295 2019-12-11T20:55:17+01:00 Download dd12174
Download 2663498 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 571 2019-12-11T20:44:32+01:00 Download 01965e0
Download 794c8dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 374 2019-12-08T01:51:27+01:00 Download 1d1b4eb
Download 729d4b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 390 2019-12-04T02:58:29+01:00 Download 4a4b515
Download 036a1a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 295 2019-12-03T08:08:11+01:00 Download 9738c6a
Download 9738c6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 296 2019-11-30T07:20:54+01:00
Download d9ee02b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 296 2019-12-01T07:06:16+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ea69267 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T04:48 CET (sv-comp)
Download 8d8416d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 12 2018-12-08T13:47:46
Download 83f346c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 100 2018-12-07T10:24 CET (sv-comp)
Download 5e4256b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 298 2018-12-07T02:54:10+01:00
Download dfa47b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 374 2018-12-10T20:37:06+01:00 Download be38cd5
Download c6ddbc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 295 2018-12-09T18:21:08+01:00 Download e3cef0a
Download d13584e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 299 2018-12-08T23:44:43+01:00 Download ea69267
Download 7fd79fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 295 2018-12-08T22:09:56+01:00 Download 8d8416d
Download 5e3d946 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 295 2018-12-08T07:45:50+01:00 Download 5e4256b
Download 89aeb85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 295 2018-12-08T05:06:17+01:00 Download 9791942
Download 936de68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 390 2018-12-07T17:45:48+01:00 Download 83f346c
Download 40bb7c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 295 2018-12-06T10:18:46+01:00 Download 687160d
Download e6dd658 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 295 2018-12-06T09:48:13+01:00 Download d5caac8
Download 1b8cadb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 452 2018-12-06T09:20:08+01:00 Download df9320f
Download d5caac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 296 2018-12-05T07:48:56+01:00
Download 05eac79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 685 2018-12-09T20:53:16+01:00 Download 004e7b3
Download 3bc2b54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 685 2018-12-09T20:36:56+01:00 Download 411663b

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5ee87e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-03T01:50 CET (sv-comp)
Download dcb5d09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-01T23:01 CET (sv-comp)
Download b588a12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T16:19:34.320527
Download 5f2270b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T09:13:50.993654
Download db9d2e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 19 2017-12-01T04:24 CET (sv-comp)
Download e4a6356 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 171 2017-12-01T00:37:18+01:00
Download 6f39163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 612 2017-11-30T22:14:09+01:00
Download 11cb3da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 133 2017-12-01T03:53 CET (sv-comp)
Download f34c0ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 291 2017-12-02T01:03Z
Download f197a40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 113 2017-11-30T11:25 CET (sv-comp)

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

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

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

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