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/transmitter.15_false-unreach-call_false-termination.cil.c
programSHA 64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99
witnessName results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-reachsafety.transmitter.15_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA 3de64e207f9c178a13e2388527a7e63760e71d3ffbd2b73a0818ef578b850613

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:48:02+01:00
inputwitnesshash a62995f0b87bb69342e0d47f6e103c7ba9c53460cdb57a57dcb6735b802440b6
producer CPAchecker 1.7-svn 29852
program-sha256 64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99
programfile ../../sv-benchmarks/c/systemc/transmitter.15_false-unreach-call_false-termination.cil.c
programhash 64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3de64e207f9c178a13e2388527a7e63760e71d3ffbd2b73a0818ef578b850613.graphml
witness-sha256 3de64e207f9c178a13e2388527a7e63760e71d3ffbd2b73a0818ef578b850613
witness-size 93092
witness-type violation_witness

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

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

Trying to find witnesses for program (64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99, sv-benchmarks/c/systemc/transmitter.15_false-unreach-call_false-termination.cil.c).

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

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

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

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

Found 15 witnesses for program sv-benchmarks/c/systemc/transmitter.15_false-unreach-call_false-termination.cil.c, 64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c796604 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 03:51:34
Download ba08241 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 53 2019-12-03T22:53 CET (comp)
Download 8fd8a45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 93 2019-12-11T21:50:35+01:00 Download bc0a22a
Download 84854f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 135 2019-12-11T21:43:39+01:00 Download fa6031f
Download 19676a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 93 2019-12-11T21:09:43+01:00 Download c796604
Download 0817461 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 93 2019-12-11T20:55:02+01:00 Download 1f11686
Download 6a4e38c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 135 2019-12-11T20:44:52+01:00 Download 951b751
Download 0b51c1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 93 2019-12-08T00:27:20+01:00 Download fbdaa60
Download 6e0f09e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 93 2019-12-07T21:16:00+01:00 Download cfff607
Download 45d39b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 93 2019-12-04T02:58:26+01:00 Download ba08241
Download 84f547f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 93 2019-12-03T08:10:16+01:00 Download f13e817
Download f13e817 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 92 2019-11-30T04:35:44+01:00
Download fa6031f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 134 2019-11-30T22:26:42+01:00
Download 6ffe85f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 156 2019-12-08T01:51:39+01:00 Download 64c2a62
Download 4cffab7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 155 2019-12-05T20:21:52+01:00 Download 7d7eb56

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

Trying to find witnesses for program (64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99, sv-benchmarks/c/systemc/transmitter.15_false-unreach-call_false-termination.cil.c).

Found 15 witnesses for program sv-benchmarks/c/systemc/transmitter.15_false-unreach-call_false-termination.cil.c, 64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bec6617 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T07:28 CET (sv-comp)
Download 612e889 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 14 2018-12-08T06:39:07
Download d742a25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 94 2018-12-08T04:07:40+01:00
Download 2c4a472 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-09T20:19:59+01:00 Download e929eee
Download 02e2b5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 135 2018-12-09T18:20:19+01:00 Download 92d1545
Download aa000ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-08T23:44:45+01:00 Download bec6617
Download 69befad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-08T22:09:49+01:00 Download 612e889
Download 4aaf6e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-08T08:04:14+01:00 Download d742a25
Download c0c1fe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-08T05:05:42+01:00 Download 7ae67a0
Download bd6f50d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-06T10:18:30+01:00 Download a663e28
Download 3de64e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-06T09:48:02+01:00 Download a62995f
Download e30e248 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 93 2018-12-06T09:16:06+01:00 Download 3ab8ad3
Download 68531fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 135 2018-12-06T09:11:46+01:00 Download 26d4176
Download a62995f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 92 2018-12-05T18:26:09+01:00
Download 9bcb447 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 156 2018-12-10T20:38:03+01:00 Download 75a9500

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

Trying to find witnesses for program (64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99, sv-benchmarks/c/systemc/transmitter.15_false-unreach-call_false-termination.cil.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 90b6684 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 49 Sun Dec 3 01:37:34 2017
Download 5e93e64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 128 2017-12-02T23:46Z
Download 71c45e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T01:15 CET (sv-comp)
Download 0e44523 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 126 2017-12-02T10:18Z
Download 48872e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T23:04:20.243999
Download 96c8d62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T14:16:37.005652
Download eeaf468 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 29 2017-12-01T18:42 CET (sv-comp)
Download ebe47f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 29 2017-11-30T23:19 CET (sv-comp)
Download 052e6ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 82 2017-11-30T17:13:45+01:00
Download 53f6b52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 191 2017-11-30T19:05:30+01:00
Download 66dbad0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 94 2017-11-30T22:58:39+01:00
Download 4f590eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 49 2017-12-01T00:11 CET (sv-comp)
Download 7afd103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 128 2017-12-02T12:58Z

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

Trying to find witnesses for program (64f5f2829b6b927f2a11f2e227c582a8d207d79e1947d5fb0977cb1bc25d9a99, sv-benchmarks/c/systemc/transmitter.15_false-unreach-call_false-termination.cil.c).

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

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