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/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c
programSHA 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
witnessName results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c.files/witness.graphml
witnessSHA ed587b7fedc15bed58128633bd3ee338152d0d3c1e86c4bfe2fb91291763c6ab

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T01:20:30.918861
producer ESBMC 4.6.0 kind
program-sha256 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c
programhash 8044e0aeebe72762497fc5ccaff76a34eb4c9821
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ed587b7fedc15bed58128633bd3ee338152d0d3c1e86c4bfe2fb91291763c6ab.graphml
witness-sha256 ed587b7fedc15bed58128633bd3ee338152d0d3c1e86c4bfe2fb91291763c6ab
witness-size 23602
witness-type violation_witness

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

Trying to find witnesses for program (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.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 (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.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 (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.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 (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.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 (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2b4afaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 4 2019-12-01 21:50:06
Download 9a85df7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 127 2019-12-04T00:20 CET (comp)
Download 3944e53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 195 2019-12-11T21:09:29+01:00 Download 2b4afaf
Download 2ea8e82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 195 2019-12-08T01:51:22+01:00 Download 67de68a
Download fbac4be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 195 2019-12-03T08:01:03+01:00 Download f7a32b0
Download f7a32b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 198 2019-11-30T02:07:06+01:00
Download 67de68a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 157 2019-12-07T15:05:47+01:00
Download 37a3002 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 195 2019-12-01T10:27:18+01:00
Download 921227e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-11T21:41:08+01:00 Download 37a3002
Download 269090b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-11T20:54:54+01:00 Download 6e3a052
Download b98a349 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-11T20:45:48+01:00 Download d9cb3fa
Download 8d632d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-05T20:21:36+01:00 Download cf5db03
Download 946c33f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-05T19:34:02+01:00 Download 980d5cf
Download 678d3d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 34 2019-12-04T02:58:18+01:00 Download 9a85df7
Download ca83dab Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 11:10:47
Download e1f6b79 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:47 CET (comp)

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

Trying to find witnesses for program (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7a24c6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-07T23:15 CET (sv-comp)
Download 6c21746 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 51 2018-12-07T21:16:32
Download 1f7437b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 197 2018-12-07T15:26:42+01:00
Download 484c404 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 195 2018-12-08T23:43:31+01:00 Download 7a24c6e
Download c4eae55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 195 2018-12-08T09:02:13+01:00 Download 1f7437b
Download 4d6dc3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 196 2018-12-08T04:29:49+01:00 Download fd8d58b
Download a0dcaa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 195 2018-12-06T09:48:24+01:00 Download d741f7e
Download d741f7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 198 2018-12-05T19:05:22+01:00
Download c2aa292 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 35 2018-12-10T20:38:10+01:00 Download 257d41b
Download c16075a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 35 2018-12-09T18:22:33+01:00 Download 953cc34
Download 8469dfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-08T22:11:18+01:00 Download 6c21746
Download e8659bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-08T05:04:50+01:00 Download 7e828f5
Download d40b181 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T10:18:44+01:00 Download 5a8a5b8
Download 7673a33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T09:42:48+01:00 Download fdcd51d
Download 6eab3a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-06T09:06:41+01:00 Download a1693e0
Download f952a68 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T01:55 CET (sv-comp)
Download 5d3a526 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T20:18 CET (sv-comp)

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

Trying to find witnesses for program (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b9ebbdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 136 Sat Dec 2 21:44:33 2017
Download a244642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2017-12-02T12:45 CET (sv-comp)
Download ed587b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 24 2017-12-02T01:20:30.918861
Download 1cf1450 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 24 2017-12-01T13:21:17.865571
Download 9a0ff27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 64 2017-12-01T16:11 CET (sv-comp)
Download b7b277b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 63 2017-12-01T01:53 CET (sv-comp)
Download 6578b55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 195 2017-11-30T13:58:37+01:00
Download cf6f76f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 115 2017-12-01T21:02:20+01:00
Download 5c835dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 142 2017-11-30T20:37 CET (sv-comp)
Download 0ea2c22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 118 2017-11-30T22:16 CET (sv-comp)
Download a2f9b41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:50:56.401989
Download fed129e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:44:59.217828
Download f702610 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 220 2017-12-01T13:03 CET (sv-comp)
Download f18ab85 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 68 2017-12-01T14:23 CET (sv-comp)

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

Trying to find witnesses for program (04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f, sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, 04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/04efddf0cae4be5e012cc7685ae2c9cfce7c723fc704805faaac5ab6c836b23f.json

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