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/pthread-wmm/mix034_tso.opt_false-unreach-call.i
programSHA 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
witnessName results-verified/cpa-bam-slicing.2017-12-01_0846.logfiles/sv-comp18.mix034_tso.opt_false-unreach-call.i.files/witness.graphml
witnessSHA 4155a56f8baa786f78455aebb44e9017fcb9cf7e1178aca0d3c020ce3390f3d9

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T08:46:38+01:00
producer CPAchecker 1.6.1-svn 26758M
program-sha256 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
programfile ../../sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i
programhash 957f139f0b65b272965e1ab3f33f2b98232837f4
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/4155a56f8baa786f78455aebb44e9017fcb9cf7e1178aca0d3c020ce3390f3d9.graphml
witness-sha256 4155a56f8baa786f78455aebb44e9017fcb9cf7e1178aca0d3c020ce3390f3d9
witness-size 12340
witness-type correctness_witness

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

Trying to find witnesses for program (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.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 (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.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 (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.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 (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.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 (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.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 '19

Trying to find witnesses for program (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 68d6e0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T16:24:32
Download 93fe78c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 20 2018-12-07T12:22:08+01:00
Download cc799b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-09T21:49:43+01:00 Download 15b915e
Download 0002df4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-09T21:38:36+01:00 Download 6232155
Download 327f075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-08T08:48:52+01:00 Download 93fe78c
Download 36fe459 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 77 2018-12-08T05:06:10+01:00 Download 68cbfd0
Download efe56ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 103 2018-12-08T03:59:13+01:00 Download 281f1f5
Download b1e7919 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-06T19:28:35+01:00 Download f9f35c6
Download de2ddb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 77 2018-12-06T10:18:24+01:00 Download 97585fd
Download 3638aa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T09:48:48+01:00 Download bc5a3b2
Download e81395d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 103 2018-12-06T09:16:45+01:00 Download 323d33e
Download 5ac6abe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 103 2018-12-06T09:16:06+01:00 Download 323d33e
Download bc5a3b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-05T15:42:37+01:00
Download fa799e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-09T20:53:26+01:00 Download e7e9b96
Download c74aebf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-09T20:35:58+01:00 Download f5d4bcc
Download 3d156e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-08T22:10:57+01:00 Download 68d6e0f

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

Trying to find witnesses for program (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 8 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 61e625c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Yogar-CBMC 1.0 13 2017-12-03T06:10 CET (sv-comp)
Download fbb7ff8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T15:49:14.147325
Download 8a6aafa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T01:23:37.399588
Download ea4e46f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 20 2017-12-01T10:25 CET (sv-comp)
Download 4c695fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 18 2017-12-01T10:06:18+01:00
Download 323d33e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 3 2017-12-01T10:07 CET (sv-comp)
Download 34126e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 17 2017-12-01T08:48:28+01:00 aecf95c
Download 4155a56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 12 2017-12-01T08:46:38+01:00

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

Trying to find witnesses for program (94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e, sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/pthread-wmm/mix034_tso.opt_false-unreach-call.i, 94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/94ad02ad5fb8bbeffde2f491035d5d2e3082aab6c27f81337507458b85dea42e.json

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