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.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c
programSHA 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
witnessName results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c.files/witness.graphml
witnessSHA e8ab1a173aa92bc3ea6d9ee29b9ac4732944d329b6cda5695c0fd7ab35afc442

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T22:36 CET (sv-comp)
producer 2LS
program-sha256 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c
programhash 4407e3fc64a6f907cafcdd6d7121e5891f520f37
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e8ab1a173aa92bc3ea6d9ee29b9ac4732944d329b6cda5695c0fd7ab35afc442.graphml
witness-sha256 e8ab1a173aa92bc3ea6d9ee29b9ac4732944d329b6cda5695c0fd7ab35afc442
witness-size 294069
witness-type violation_witness

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

Trying to find witnesses for program (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.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 (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.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 (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.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 (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.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 (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 9 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 78d0412 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 509 2019-12-11T21:54:00+01:00 Download 2547e26
Download 2bdc3ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 509 2019-12-03T08:09:51+01:00 Download f8b01a9
Download f8b01a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 517 2019-11-29T15:19:37+01:00
Download 2547e26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 510 2019-11-30T20:28:12+01:00
Download c58f083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 58 2019-12-11T20:55:00+01:00 Download 35153d3
Download 8b397e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 60 2019-12-11T20:46:10+01:00 Download 3b887d4
Download 625c796 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 60 2019-12-08T01:52:36+01:00 Download 7e8331f
Download 449885c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 58 2019-12-05T20:20:16+01:00 Download 07a6738
Download e5ff70c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 58 2019-12-05T19:34:05+01:00 Download e9ffe3f

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

Trying to find witnesses for program (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d8ff17e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 12 2018-12-08T17:04 CET (sv-comp)
Download 328b703 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 133 2018-12-08T11:04:04
Download b760d83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 514 2018-12-06T12:47:47+01:00
Download cb0ad94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 508 2018-12-08T23:42:05+01:00 Download d8ff17e
Download 1409d0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 509 2018-12-08T08:40:32+01:00 Download b760d83
Download 0f39fbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 509 2018-12-06T09:48:25+01:00 Download bfb63e4
Download bfb63e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 516 2018-12-06T06:05:42+01:00
Download ce90bad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 60 2018-12-10T20:37:35+01:00 Download 70c92fa
Download 134018d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 60 2018-12-09T18:21:58+01:00 Download 2bcfc03
Download 66578d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 58 2018-12-08T22:07:27+01:00 Download 328b703
Download 514a306 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 60 2018-12-08T04:54:50+01:00 Download b94c9b1
Download 73ccd85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 60 2018-12-06T10:14:07+01:00 Download 8a2f1e1
Download 1357b16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 58 2018-12-06T09:41:11+01:00 Download b5c7801
Download 249dc23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 58 2018-12-06T09:15:27+01:00 Download 488eb60

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

Trying to find witnesses for program (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 8 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9a5627d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 338 Sat Dec 2 22:16:43 2017
Download ef9a97d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 12 2017-12-01T23:48 CET (sv-comp)
Download 49e2325 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 60 2017-12-02T01:13:49.578623
Download 0075a44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 61 2017-12-01T07:52:44.912166
Download f959955 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 158 2017-12-01T04:34 CET (sv-comp)
Download 02c35d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 503 2017-12-01T03:44:51+01:00
Download 74bb3ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 353 2017-11-30T22:07 CET (sv-comp)
Download e8ab1a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 294 2017-11-30T22:36 CET (sv-comp)

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

Trying to find witnesses for program (97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f, sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/97750343adcd42c7e6a74ffa2dc343e1b09ec32d119b650d64e455b937a71a1f.json

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