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/systemc/bist_cell_true-unreach-call_false-termination.cil.c
programSHA ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
witnessName results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-reachsafety.bist_cell_true-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA ce8514fa3ae9a452bda1a9212cfe5b99265ba2bf5284a0bfd93294d3fa0c9874

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T00:50Z
producer Taipan
programfile /tmp/vcloud-vcloud-master/worker/working_dir_c92b2853-14b7-4051-bce7-5306727bfe67/sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c
programhash bb52621d262b2a79ebd79f9601fb8103d2f4f11e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ce8514fa3ae9a452bda1a9212cfe5b99265ba2bf5284a0bfd93294d3fa0c9874.graphml
witness-sha256 ce8514fa3ae9a452bda1a9212cfe5b99265ba2bf5284a0bfd93294d3fa0c9874
witness-size 60539
witness-type correctness_witness

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

Trying to find witnesses for program (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.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 (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.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 (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.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 (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.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 (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 11 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b46a6ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 40 2019-12-11T20:09:18+01:00 Download ba2ce5b
Download 2f3e473 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 40 2019-12-08T01:01:59+01:00 Download d4e0124
Download 6886a4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 40 2019-12-07T23:41:39+01:00 Download 4d0d17c
Download fff9e67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 40 2019-12-07T19:47:41+01:00 Download 49db15c
Download 622f1f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 40 2019-12-05T19:02:52+01:00 Download 232a1fe
Download eb3a0d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 40 2019-11-30T17:28:29+01:00 Download 13fe384
Download 13fe384 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 40 2019-11-30T05:06:37+01:00
Download d4e0124 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 284 2019-12-07T16:32:58+01:00
Download ba2ce5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 41 2019-12-01T06:15:03+01:00
Download 0656151 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 33 2019-11-29T18:19:27+01:00
Download 3e2267b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 33 2019-12-01T14:19:27+01:00

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

Trying to find witnesses for program (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 6 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a4243cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T03:12:49
Download 4b22645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 40 2018-12-08T00:24:38+01:00
Download 32c54e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 41 2018-12-05T09:29:48+01:00
Download 349a2b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 32 2018-12-07T04:45:27+01:00
Download d9757ee Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 33 2018-12-09T20:36:00+01:00
Download 69c646a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 33 2018-12-05T16:43:23+01:00

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

Trying to find witnesses for program (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 13 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7362f35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 40 2017-12-03T02:41:09+01:00 0165625
Download 650be6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 40 2017-12-02T15:15:49+01:00 12c07cb
Download de3b8d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 40 2017-12-01T07:01:46+01:00 ed5ae07
Download c111474 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 40 2017-12-01T06:40:29+01:00 a3d62e0
Download a95641f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 41 2017-12-01T05:51:41+01:00 269c2a0
Download f77be11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 41 2017-11-30T18:11:48+01:00
Download 9323e06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 71 2017-11-30T17:49:09+01:00
Download 6d461a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 36 2017-12-02T08:29:49+01:00
Download be31162 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 77 2017-12-02T11:44Z
Download 32f8117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 99 2017-11-30T13:17 CET (sv-comp)
Download aecb319 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 33 2017-12-01T12:52:23+01:00
Download 6a89ee3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 55 2017-12-03T11:16Z
Download 8930437 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 30 2017-12-01T12:14 CET (sv-comp)

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

Trying to find witnesses for program (ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12, sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/bist_cell_true-unreach-call_false-termination.cil.c, ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ed7cf118393df741439bf83f6a53ce8b2b1ac944b31c04ecea3e98050f258e12.json

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