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/mix000_rmo.opt_false-unreach-call.i
programSHA 61c4a57830e1365317ed9b922c16732d232b1d8aa8040b7ef099cb05353bdfcc
witnessName results-verified/cbmc.2017-12-01_0912.logfiles/sv-comp18.mix000_rmo.opt_false-unreach-call.i.files/witness.graphml
witnessSHA bccd74e741cd0bc0f759ad8561667fdd9fe68bc69f10feb6337eb8f6f07a512c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T09:33 CET (sv-comp)
producer CBMC
program-sha256 61c4a57830e1365317ed9b922c16732d232b1d8aa8040b7ef099cb05353bdfcc
programfile ../../sv-benchmarks/c/pthread-wmm/mix000_rmo.opt_false-unreach-call.i
programhash 955793ded220663ed453216afabe04ee8e7d5e37
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/bccd74e741cd0bc0f759ad8561667fdd9fe68bc69f10feb6337eb8f6f07a512c.graphml
witness-sha256 bccd74e741cd0bc0f759ad8561667fdd9fe68bc69f10feb6337eb8f6f07a512c
witness-size 3447
witness-type violation_witness

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

Trying to find witnesses for program (61c4a57830e1365317ed9b922c16732d232b1d8aa8040b7ef099cb05353bdfcc, sv-benchmarks/c/pthread-wmm/mix000_rmo.opt_false-unreach-call.i).

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7d9cf2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T14:13:34
Download 30d2c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 25 2018-12-07T22:29:52+01:00
Download de3d0c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-09T21:47:55+01:00 Download b8f05cf
Download 4c1df88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-09T21:38:27+01:00 Download be2be49
Download 7e27ca3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-08T08:53:28+01:00 Download 30d2c9d
Download fdab7fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 36 2018-12-08T05:00:21+01:00 Download 55feeaf
Download a2bf14e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2918 2018-12-08T03:27:49+01:00 Download ba8a9e6
Download 0cec5d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 23 2018-12-06T19:52:34+01:00 Download f8755bb
Download be4e33d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 36 2018-12-06T10:13:36+01:00 Download 57f2a61
Download 7294b41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 26 2018-12-06T09:47:56+01:00 Download e91a456
Download d97334f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 241 2018-12-06T09:20:20+01:00 Download bccd74e
Download 3f7b945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 241 2018-12-06T09:16:08+01:00 Download bccd74e
Download e91a456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-06T07:33:54+01:00
Download b8a64ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-09T20:54:00+01:00 Download d91680a
Download 500297b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-09T20:39:03+01:00 Download 4fd3c2b
Download 43c6cb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 34 2018-12-08T22:10:31+01:00 Download 7d9cf2f

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

Trying to find witnesses for program (61c4a57830e1365317ed9b922c16732d232b1d8aa8040b7ef099cb05353bdfcc, sv-benchmarks/c/pthread-wmm/mix000_rmo.opt_false-unreach-call.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 175e3ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Yogar-CBMC 1.0 15 2017-12-03T06:01 CET (sv-comp)
Download 8251ade Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T15:07:42.005183
Download 33a9eaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-02T04:05:08.652363
Download b86fb9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 23 2017-12-01T12:28 CET (sv-comp)
Download eae4296 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 23 2017-12-01T10:08:54+01:00
Download bccd74e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 3 2017-12-01T09:33 CET (sv-comp)
Download 8678620 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 35 2017-12-01T08:48:27+01:00 dded38b
Download 3a2f4b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 14 2017-12-01T08:46:21+01:00

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

Trying to find witnesses for program (61c4a57830e1365317ed9b922c16732d232b1d8aa8040b7ef099cb05353bdfcc, sv-benchmarks/c/pthread-wmm/mix000_rmo.opt_false-unreach-call.i).

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

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