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.13_false-unreach-call_false-termination.cil.c
programSHA 8023c8e728395dd2adcb0a26db888824f99490e2ad28c47b8aa7557c165044f1
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.transmitter.13_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA a56495e489a2f9ac9e5a5d6171f5fa1e410583ef35318c03d1e475e4291b7e03

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T00:23 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 8023c8e728395dd2adcb0a26db888824f99490e2ad28c47b8aa7557c165044f1
programfile /tmp/vcloud-vcloud-master/worker/working_dir_1ecf454a-c0be-4f36-9b94-4d2514b6d8fe/sv-benchmarks/c/systemc/transmitter.13_false-unreach-call_false-termination.cil.c
programhash d9aace3d5003f6dd455a09e747d58ecec63822ab
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a56495e489a2f9ac9e5a5d6171f5fa1e410583ef35318c03d1e475e4291b7e03.graphml
witness-sha256 a56495e489a2f9ac9e5a5d6171f5fa1e410583ef35318c03d1e475e4291b7e03
witness-size 171070
witness-type violation_witness

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

Trying to find witnesses for program (8023c8e728395dd2adcb0a26db888824f99490e2ad28c47b8aa7557c165044f1, sv-benchmarks/c/systemc/transmitter.13_false-unreach-call_false-termination.cil.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1e7bb45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 843 2019-12-11T21:46:08+01:00 Download 83a9f2f
Download 8039753 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 843 2019-12-11T20:55:31+01:00 Download 4ec2a97
Download 294db64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 942 2019-12-11T20:44:36+01:00 Download 61d8799
Download 6b03e81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 843 2019-12-03T08:10:24+01:00 Download eeee834
Download eeee834 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 796 2019-11-30T00:33:55+01:00
Download 83a9f2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 843 2019-12-01T16:50:42+01:00
Download d3e5e36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 156 2019-12-08T01:51:27+01:00 Download 2c32056
Download f7117b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 155 2019-12-05T20:20:45+01:00 Download 537aa9f

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

Trying to find witnesses for program (8023c8e728395dd2adcb0a26db888824f99490e2ad28c47b8aa7557c165044f1, sv-benchmarks/c/systemc/transmitter.13_false-unreach-call_false-termination.cil.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 874f6c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T11:54 CET (sv-comp)
Download 24b701d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 95 2018-12-08T13:10:39
Download c46ca45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 789 2018-12-07T20:25:18+01:00
Download de2ec90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 942 2018-12-09T17:49:07+01:00 Download 8cd5f23
Download 7e9fb40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 844 2018-12-08T23:44:47+01:00 Download 874f6c3
Download bb0977c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 843 2018-12-08T22:11:29+01:00 Download 24b701d
Download e1ffee2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 843 2018-12-08T08:05:24+01:00 Download c46ca45
Download 0a7eac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 863 2018-12-08T05:03:03+01:00 Download 0bf8dde
Download 6a491bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 843 2018-12-06T09:48:30+01:00 Download c202419
Download f51ede9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 843 2018-12-06T09:11:26+01:00 Download 4661c27
Download c202419 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 796 2018-12-06T00:36:55+01:00
Download 9bd957f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 156 2018-12-10T20:38:06+01:00 Download f7dbb5f
Download d7316df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 155 2018-12-06T10:15:33+01:00 Download 0a3865c

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

Trying to find witnesses for program (8023c8e728395dd2adcb0a26db888824f99490e2ad28c47b8aa7557c165044f1, sv-benchmarks/c/systemc/transmitter.13_false-unreach-call_false-termination.cil.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7ca515f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 410 Sat Dec 2 17:27:06 2017
Download 90bbb51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T01:01 CET (sv-comp)
Download 6819b71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 12 2017-12-01T21:00:30.966533
Download 62b2b9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 24 2017-12-01T08:10:52.483455
Download 18989c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 171 2017-12-01T19:03 CET (sv-comp)
Download a56495e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 171 2017-12-01T00:23 CET (sv-comp)
Download 9731c47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 718 2017-11-30T22:14:37+01:00
Download a47b775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 400 2017-11-30T20:27 CET (sv-comp)

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

Trying to find witnesses for program (8023c8e728395dd2adcb0a26db888824f99490e2ad28c47b8aa7557c165044f1, sv-benchmarks/c/systemc/transmitter.13_false-unreach-call_false-termination.cil.c).

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

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