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/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c
programSHA 4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2
witnessName results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.mem_slave_tlm.1_true-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA a5efc65513fa88b8ddef33e697c881cdb2dd2193c69a39c8ce9affab0cb9e82c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T03:01:32+01:00
producer CPAchecker 1.6.1-svn 26725
program-sha256 4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2
programfile ../../sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c
programhash fbecaa911234564619645b897eed5716f7c8acd9
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a5efc65513fa88b8ddef33e697c881cdb2dd2193c69a39c8ce9affab0cb9e82c.graphml
witness-sha256 a5efc65513fa88b8ddef33e697c881cdb2dd2193c69a39c8ce9affab0cb9e82c
witness-size 116453
witness-type correctness_witness

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

Trying to find witnesses for program (4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2, sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c).

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

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

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

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

Found 8 witnesses for program sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c, 4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0d049bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 116 2019-12-11T20:18:36+01:00 Download 583f4a7
Download a3bc2c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 116 2019-12-08T00:36:34+01:00 Download 8ed3e55
Download cab117e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 116 2019-12-07T19:46:57+01:00 Download 49595a0
Download d4ee710 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 116 2019-11-30T17:12:47+01:00 Download f2151b4
Download f2151b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 117 2019-11-30T06:30:36+01:00
Download 583f4a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 117 2019-11-30T20:42:23+01:00
Download 4cd36d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 107 2019-11-29T14:37:48+01:00
Download 63d0844 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 107 2019-11-30T23:12:03+01:00

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

Trying to find witnesses for program (4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2, sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c).

Found 9 witnesses for program sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c, 4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ede0328 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 116 2018-12-08T03:27:03+01:00
Download 60e82f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-10T20:09:43+01:00 Download f85391a
Download 2e606b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-09T20:21:50+01:00 Download eaae6c9
Download 4c6627c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-08T07:22:32+01:00 Download ede0328
Download b2b0a15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-06T09:05:52+01:00 Download 6a462f6
Download 6a462f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 117 2018-12-06T05:21:27+01:00
Download d667b07 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 107 2018-12-06T13:28:47+01:00
Download 61b79bc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 108 2018-12-09T20:37:35+01:00
Download 05a6682 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 107 2018-12-05T15:40:56+01:00

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

Trying to find witnesses for program (4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2, sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c).

Found 10 witnesses for program sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c, 4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 049d630 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 116 2017-12-02T15:23:11+01:00 7458e69
Download 48c7945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 116 2017-12-01T07:22:59+01:00 2f2578e
Download 426ad14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 116 2017-12-01T05:43:56+01:00 0057a7c
Download 6b1ed96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 116 2017-12-01T04:41:23+01:00 455400f
Download fd6a4be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 117 2017-11-30T16:42:03+01:00
Download 9b9ffb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 182 2017-12-01T00:03:57+01:00
Download a5efc65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 116 2017-12-01T03:01:32+01:00
Download 142e81c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 10 2017-12-02T04:27:32+01:00
Download bfdbe72 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 107 2017-12-01T13:36:13+01:00
Download 6ef451e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 35 2017-12-03T11:14Z

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

Trying to find witnesses for program (4667155585f57897f599de75134aa519f0d36bbb66ce64c9d2a621f67f9be9a2, sv-benchmarks/c/systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c).

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

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