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.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programSHA a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
witnessName results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-reachsafety.pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c.files/witness.graphml
witnessSHA ba866bf9e081b76f26856cdf852f9dc3fe39b9780354552e420d99719ee2421d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:49:19+01:00
inputwitnesshash 7a036014bc7e820fc951cf76a18d6e20c3f74de0c0c78ad976bb936dffc67bea
producer CPAchecker 1.7-svn 29852
program-sha256 a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c
programhash a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ba866bf9e081b76f26856cdf852f9dc3fe39b9780354552e420d99719ee2421d.graphml
witness-sha256 ba866bf9e081b76f26856cdf852f9dc3fe39b9780354552e420d99719ee2421d
witness-size 116796
witness-type violation_witness

This witness was created for this program (cf. table above, a8efe39bb66f2edaea4f8b0c0914ba1115ab71d776ec4bb20ba56c660486fd56).

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 41f972a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 80 2019-12-04T00:40 CET (comp)
Download c205d01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 112 2019-12-11T21:58:06+01:00 Download 0f81d30
Download bc71232 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 114 2019-12-11T21:44:20+01:00 Download ea9e391
Download 02525d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 114 2019-12-11T20:44:50+01:00 Download 2380c50
Download a4722a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 117 2019-12-08T01:51:57+01:00 Download 20cb2c8
Download 4a98298 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 112 2019-12-07T21:14:50+01:00 Download 409e7fb
Download e9b3651 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 118 2019-12-03T08:57:33+01:00 Download 984d46f
Download 172d0a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 117 2019-12-03T08:07:32+01:00 Download 7d8dd46
Download 7d8dd46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 120 2019-11-30T02:27:57+01:00
Download 20cb2c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 93 2019-12-07T14:10:31+01:00
Download ea9e391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 115 2019-12-01T00:55:30+01:00
Download ff8e805 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 32 2019-12-11T21:09:33+01:00 Download 0ec7326
Download 77bf1e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 32 2019-12-11T20:55:21+01:00 Download 020304c
Download 48b6303 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 32 2019-12-05T20:20:26+01:00 Download 00c1335
Download 9ffe352 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 33 2019-12-05T19:34:25+01:00 Download 161eca6
Download f741ee5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 33 2019-12-04T02:58:15+01:00 Download 41f972a
Download 206a876 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 10:38:30

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5bb2fd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T03:23 CET (sv-comp)
Download 98c552f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 29 2018-12-08T00:40:58
Download 193c3b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 115 2018-12-08T02:31:35+01:00
Download 7d5b127 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 112 2018-12-09T20:27:45+01:00 Download 55e0fc3
Download edb40f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 114 2018-12-09T18:21:04+01:00 Download 0f94912
Download 8d66bee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 111 2018-12-08T23:43:08+01:00 Download 5bb2fd7
Download 5fbbc38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 114 2018-12-08T08:55:29+01:00 Download 193c3b6
Download 9862df8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 118 2018-12-08T03:48:39+01:00 Download ed4b2a9
Download ba866bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 117 2018-12-06T09:49:19+01:00 Download 7a03601
Download 7a03601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 120 2018-12-05T10:54:05+01:00
Download 2744fd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-10T20:37:43+01:00 Download ff1d21b
Download 2d3479c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 32 2018-12-08T22:10:45+01:00 Download 98c552f
Download c811a62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-08T04:59:07+01:00 Download 67e71d4
Download d5cc022 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-06T10:18:08+01:00 Download 6a185eb
Download 01b2f8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-06T09:41:48+01:00 Download 180f32a
Download d19786a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 32 2018-12-06T09:16:36+01:00 Download 3b74133

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 368fe88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 82 Sun Dec 3 00:35:53 2017
Download 938c1d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2017-12-02T05:07 CET (sv-comp)
Download 1a6a1dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 141 2017-12-02T16:45Z
Download fd79170 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 15 2017-12-02T01:10:57.166562
Download 4274a5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 16 2017-12-01T20:32:53.944414
Download fcc4731 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 39 2017-11-30T16:33 CET (sv-comp)
Download d18f413 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 116 2017-11-30T14:58:05+01:00
Download 3c48fe9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 74 2017-12-01T22:45:01+01:00
Download 29e5b14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 86 2017-11-30T12:56 CET (sv-comp)
Download d32efcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 72 2017-11-30T16:09 CET (sv-comp)

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

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

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

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