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-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programSHA 2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml
witnessSHA ec18aa7b3268b76f50c8c9304ac324fa82c669c82952035ef033698509d54e67

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T07:31 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135
programfile /tmp/vcloud-vcloud-master/worker/working_dir_bd0cc50e-a9e9-4d4d-8b42-8ff864602392/sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programhash 8ef6b88f405ba179e410ad54d9a35e6983c3e141
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ec18aa7b3268b76f50c8c9304ac324fa82c669c82952035ef033698509d54e67.graphml
witness-sha256 ec18aa7b3268b76f50c8c9304ac324fa82c669c82952035ef033698509d54e67
witness-size 58081
witness-type violation_witness

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

Trying to find witnesses for program (2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ce490be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 125 2019-12-03T23:41 CET (comp)
Download ff960c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 184 2019-12-11T21:52:16+01:00 Download 628ca08
Download c684c4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 182 2019-12-11T20:44:48+01:00 Download eb4182b
Download 0586b52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 184 2019-12-03T08:09:41+01:00 Download 41942c6
Download 41942c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 187 2019-11-30T06:10:35+01:00
Download 628ca08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 185 2019-11-30T21:41:36+01:00
Download 1f515f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 41 2019-12-11T21:09:01+01:00 Download 53af3f1
Download 20aa513 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 41 2019-12-11T20:54:55+01:00 Download 3f24862
Download ed82269 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 42 2019-12-08T01:51:17+01:00 Download 2dfdea3
Download e1a1f28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 41 2019-12-05T20:20:43+01:00 Download c783150
Download 6f75c04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 42 2019-12-05T19:34:51+01:00 Download 977a7e6
Download 5f78d6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 43 2019-12-04T02:58:05+01:00 Download ce490be
Download f7d5757 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 5 2019-12-01 20:12:45

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

Trying to find witnesses for program (2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e41d6c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 10 2018-12-08T06:11 CET (sv-comp)
Download c0fa657 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 45 2018-12-08T07:09:38
Download aa848d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 186 2018-12-07T01:25:39+01:00
Download 45f7419 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 182 2018-12-09T17:53:46+01:00 Download 83f20b7
Download 7ec509f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 177 2018-12-08T23:41:57+01:00 Download e41d6c4
Download cc6fd7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-08T08:48:04+01:00 Download aa848d3
Download 9a5b22e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-06T09:49:21+01:00 Download 84551d1
Download 84551d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-05T18:42:59+01:00
Download 68c7a2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 42 2018-12-10T20:37:36+01:00 Download 5c95106
Download 16bfcbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 42 2018-12-08T22:09:19+01:00 Download c0fa657
Download 708ecc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 42 2018-12-08T04:57:08+01:00 Download 43bb3b7
Download e04d18e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 42 2018-12-06T10:17:20+01:00 Download b9c6a19
Download 8c823e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 42 2018-12-06T09:43:37+01:00 Download 607de35
Download 5b54b9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 41 2018-12-06T09:19:00+01:00 Download 2fb8da7

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

Trying to find witnesses for program (2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 9 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 927a1d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 132 Sat Dec 2 18:38:18 2017
Download e8adef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 10 2017-12-02T02:43 CET (sv-comp)
Download b885433 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 23 2017-12-01T16:20:20.136948
Download 86193c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 24 2017-12-01T10:48:48.763097
Download ec18aa7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 58 2017-12-01T07:31 CET (sv-comp)
Download 46f4c09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 181 2017-11-30T20:33:31+01:00
Download 45921e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 122 2017-12-02T07:27:43+01:00
Download d95f245 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 138 2017-12-01T03:14 CET (sv-comp)
Download 5d88c0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 116 2017-11-30T14:46 CET (sv-comp)

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

Trying to find witnesses for program (2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c, 2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2248cdcf84be69418e94c00fe805c91d99d99538a2952a5d17a79d0e17db8135.json

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