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/token_ring.11_false-unreach-call_false-termination.cil.c
programSHA 5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.token_ring.11_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA 439f35fae812a66317e405f7842f1887a800b9de4595a6c25682eb1309169293

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T05:09 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7
programfile /tmp/vcloud-vcloud-master/worker/working_dir_ee51c3c0-a540-4fa3-ad5b-02508612d41e/sv-benchmarks/c/systemc/token_ring.11_false-unreach-call_false-termination.cil.c
programhash 016d9724229fc10b14185725b324fda19eb01dcb
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/439f35fae812a66317e405f7842f1887a800b9de4595a6c25682eb1309169293.graphml
witness-sha256 439f35fae812a66317e405f7842f1887a800b9de4595a6c25682eb1309169293
witness-size 235057
witness-type violation_witness

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

Trying to find witnesses for program (5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7, sv-benchmarks/c/systemc/token_ring.11_false-unreach-call_false-termination.cil.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b833333 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 701 2019-12-11T22:00:57+01:00 Download 6ed83bc
Download 3e4e1ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2427 2019-12-11T20:54:30+01:00 Download 56ab311
Download 35989ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 713 2019-12-11T20:44:43+01:00 Download 9c251b9
Download 3ce10ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 701 2019-12-03T08:09:09+01:00 Download 46b1fa0
Download 46b1fa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 719 2019-11-30T12:47:28+01:00
Download 6ed83bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 701 2019-12-01T12:50:53+01:00
Download 26be869 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 141 2019-12-08T01:52:21+01:00 Download 959e0c7
Download 4cfcda7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 141 2019-12-05T20:20:29+01:00 Download 9c11160

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

Trying to find witnesses for program (5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7, sv-benchmarks/c/systemc/token_ring.11_false-unreach-call_false-termination.cil.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download aa7bc0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T06:36 CET (sv-comp)
Download 7b41d37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 84 2018-12-08T07:36:45
Download bcc3906 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 706 2018-12-08T02:31:33+01:00
Download df48b0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 718 2018-12-09T18:20:33+01:00 Download 285f414
Download c34ac64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 702 2018-12-08T23:41:59+01:00 Download aa7bc0e
Download cff9422 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 701 2018-12-08T22:08:28+01:00 Download 7b41d37
Download 45290f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 701 2018-12-08T08:27:16+01:00 Download bcc3906
Download f91b687 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 701 2018-12-08T05:04:00+01:00 Download 95de34f
Download 4eea06a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 701 2018-12-06T09:48:32+01:00 Download 4c7bc94
Download 9b3a8a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 739 2018-12-06T09:17:17+01:00 Download d58e523
Download 4c7bc94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 719 2018-12-05T17:22:14+01:00
Download 0e8a81a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 142 2018-12-10T20:37:32+01:00 Download bb6e168
Download f350174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 141 2018-12-06T10:15:48+01:00 Download a22e9f9

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

Trying to find witnesses for program (5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7, sv-benchmarks/c/systemc/token_ring.11_false-unreach-call_false-termination.cil.c).

Found 8 witnesses for program sv-benchmarks/c/systemc/token_ring.11_false-unreach-call_false-termination.cil.c, 5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4bcba03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 348 Sat Dec 2 22:37:44 2017
Download 2fee3a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T03:28 CET (sv-comp)
Download e33383e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 26 2017-12-01T14:35:28.272219
Download 9b024bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 26 2017-12-01T08:22:17.196883
Download 7148e6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 235 2017-12-01T19:56 CET (sv-comp)
Download 439f35f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 235 2017-12-01T05:09 CET (sv-comp)
Download be1627a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 655 2017-11-30T11:59:24+01:00
Download 683c35f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 345 2017-12-01T00:27 CET (sv-comp)

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

Trying to find witnesses for program (5899b4ce011d377672da48effb0aa2c239f486bd2860689243b43cf2a5a76da7, sv-benchmarks/c/systemc/token_ring.11_false-unreach-call_false-termination.cil.c).

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

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