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_label39_false-unreach-call.c
programSHA 67912fc827b945fba985b90b7b4af244b2bc6837c3c88b70bc61df7f1a1e6971
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.Problem03_label39_false-unreach-call.c.files/witness.graphml
witnessSHA 785ad7850faab03d52dd1c761ddcc378a091132d8f99e2eb42e20104d6a6a4ad

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T11:16:39.732866
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/eca-rers2012/Problem03_label39_false-unreach-call.c
programhash be345c87c00c2322977f292068f4516fd2aa624c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/785ad7850faab03d52dd1c761ddcc378a091132d8f99e2eb42e20104d6a6a4ad.graphml
witness-sha256 785ad7850faab03d52dd1c761ddcc378a091132d8f99e2eb42e20104d6a6a4ad
witness-size 4793
witness-type violation_witness

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

Trying to find witnesses for program (67912fc827b945fba985b90b7b4af244b2bc6837c3c88b70bc61df7f1a1e6971, sv-benchmarks/c/eca-rers2012/Problem03_label39_false-unreach-call.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4c9c55e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 01:54:53
Download 187a4dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 146 2019-12-04T00:26 CET (comp)
Download 92e1d0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 492 2019-12-11T21:52:44+01:00 Download 5eeff80
Download dd6bdc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 492 2019-12-11T21:09:11+01:00 Download 4c9c55e
Download 9ceaffe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 493 2019-12-11T20:55:12+01:00 Download 98af165
Download c95e351 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 493 2019-12-11T20:44:58+01:00 Download cbc9053
Download 3c6cc13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 495 2019-12-08T01:52:11+01:00 Download 3ae9ee6
Download 86b7b6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 657 2019-12-04T02:58:25+01:00 Download 187a4dc
Download 9798fd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 492 2019-12-03T08:10:37+01:00 Download f75b13a
Download f75b13a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 493 2019-11-30T12:06:57+01:00
Download 5eeff80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 493 2019-12-01T10:39:23+01:00
Download 950cb40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 685 2019-12-08T00:28:21+01:00 Download 77dc7b9

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

Trying to find witnesses for program (67912fc827b945fba985b90b7b4af244b2bc6837c3c88b70bc61df7f1a1e6971, sv-benchmarks/c/eca-rers2012/Problem03_label39_false-unreach-call.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 98df127 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T16:41 CET (sv-comp)
Download c5d2db9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 13 2018-12-08T07:10:12
Download 120fd56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 159 2018-12-07T05:20 CET (sv-comp)
Download c4df379 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 497 2018-12-07T09:41:11+01:00
Download 6ab8b93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 495 2018-12-10T20:37:22+01:00 Download 7419f6c
Download 970ef77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 493 2018-12-09T18:20:26+01:00 Download 461337d
Download 8d9e4f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 497 2018-12-08T23:43:29+01:00 Download 98df127
Download d7d7d36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 492 2018-12-08T22:07:30+01:00 Download c5d2db9
Download 7446d52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 492 2018-12-08T07:54:34+01:00 Download c4df379
Download 19c795a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 493 2018-12-08T05:04:39+01:00 Download 785ad78
Download 6a371bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 657 2018-12-07T17:45:50+01:00 Download 120fd56
Download 6c0f457 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 493 2018-12-06T10:16:21+01:00 Download c315b6e
Download a7b033b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 492 2018-12-06T09:48:41+01:00 Download 3ab91f5
Download 4bef4fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 658 2018-12-06T09:19:14+01:00 Download b93eadf
Download 3ab91f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 493 2018-12-05T18:46:16+01:00
Download e1cc784 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 685 2018-12-09T20:54:23+01:00 Download 81c81a1
Download ba32de1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 685 2018-12-09T20:41:16+01:00 Download 6913bf7

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

Trying to find witnesses for program (67912fc827b945fba985b90b7b4af244b2bc6837c3c88b70bc61df7f1a1e6971, sv-benchmarks/c/eca-rers2012/Problem03_label39_false-unreach-call.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 062e9f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-02T20:31 CET (sv-comp)
Download e0d6b23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T16:27 CET (sv-comp)
Download bc6eeaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T00:54:58.797948
Download eb6e659 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T16:52:18.261367
Download 9a2bb29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 21 2017-12-01T02:23 CET (sv-comp)
Download 6a064de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 282 2017-11-30T15:37:09+01:00
Download b683b0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 1085 2017-11-30T15:50:14+01:00
Download 106a34e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 276 2017-12-01T02:37:51+01:00
Download 58949e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 180 2017-11-30T20:14 CET (sv-comp)
Download ad07b5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 181 2017-11-30T23:00 CET (sv-comp)

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

Trying to find witnesses for program (67912fc827b945fba985b90b7b4af244b2bc6837c3c88b70bc61df7f1a1e6971, sv-benchmarks/c/eca-rers2012/Problem03_label39_false-unreach-call.c).

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

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