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/loops/terminator_03_false-unreach-call_true-termination.i
programSHA 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
witnessName results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-reachsafety.terminator_03_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA f357d629364bbc43cdc6ce002ca18cb0b1e0996ae43d70117bb10beb703e481e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T01:46Z
producer Kojak
programfile /tmp/vcloud-vcloud-master/worker/working_dir_157a52d1-3d3d-4f29-9d14-26ccc068519e/sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i
programhash 52ac1cbbf609460dddc737d444d8d8d12fc803ae
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/f357d629364bbc43cdc6ce002ca18cb0b1e0996ae43d70117bb10beb703e481e.graphml
witness-sha256 f357d629364bbc43cdc6ce002ca18cb0b1e0996ae43d70117bb10beb703e481e
witness-size 5043
witness-type violation_witness

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

Trying to find witnesses for program (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.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 (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.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 (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.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 (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.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 (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.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 '19

Trying to find witnesses for program (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 22 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8833dd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2018-12-08T11:45 CET (sv-comp)
Download 11d0b74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T05:33:55
Download b1dce44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 7 2018-12-10T18:30:52+01:00
Download 2d8019d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-07T19:23:09+01:00
Download e986220 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:35:03+01:00 Download b1dce44
Download 69ed3a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:20+01:00 Download ca6ac90
Download 09a07ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:39:44+01:00 Download 07689f7
Download badbc88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:18:59+01:00 Download f357d62
Download f63733d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T18:21:39+01:00 Download 1a45449
Download 78b5697 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:43:04+01:00 Download 8833dd1
Download 4c26714 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T07:57:35+01:00 Download 2d8019d
Download c0baf18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T05:04:14+01:00 Download ec69ec9
Download abb1036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T03:59:07+01:00 Download 37a16a0
Download f88f50a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T18:48:33+01:00 Download 55e6791
Download b6608e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:23:47+01:00 Download 7cef3e9
Download e96c9fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T10:19:11+01:00 Download e63b6bd
Download 04a72dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:48:03+01:00 Download d307bda
Download 857d23b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:41:35+01:00 Download bf74630
Download 14eb3a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:10:35+01:00 Download f49ef48
Download 4d82527 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:10:28+01:00 Download 2389d61
Download d307bda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T04:03:59+01:00
Download fc9d934 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T22:09:35+01:00 Download 11d0b74

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

Trying to find witnesses for program (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 34e6410 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:26 CET (sv-comp)
Download b8994f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 34 2017-12-03T04:06 CET (sv-comp)
Download 7df61b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-03T04:58Z
Download 7f2cef1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:36 CET (sv-comp)
Download e82eb6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T20:18 CET (sv-comp)
Download 6ee8eb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 5 2017-12-02T09:37Z
Download 8c71a08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T05:35:16.092087
Download abdf62c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T08:53:29.761098
Download a4febee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T16:26 CET (sv-comp)
Download ac3cc1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T02:43 CET (sv-comp)
Download 66826fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 6 2017-12-03T03:21:53+01:00
Download 4707244 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T14:21:09+01:00
Download 972a761 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T21:56:15+01:00
Download 123a838 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-12-01T03:48:29+01:00
Download a9b4dfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T08:25:27+01:00
Download 2e2f010 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 5 2017-11-30T17:12 CET (sv-comp)
Download 154b29e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T00:16Z
Download bf74630 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T21:38 CET (sv-comp)

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

Trying to find witnesses for program (2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952, sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/terminator_03_false-unreach-call_true-termination.i, 2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2a2f03f3b15bb4c1e4a2ed1473a2abf6bcbd1ebfb151968987ffded89a0c4952.json

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