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/nec20_false-unreach-call_true-termination.i
programSHA 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
witnessName results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.nec20_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 5cf0008d584127d4e820147838bde31e93b56f6bd1f253fb130be9ff756107d7

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T14:32 CET (sv-comp)
producer Symbiotic
program-sha256 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
programfile /tmp/vcloud-vcloud-master/worker/working_dir_fac9b28b-e0e0-44f2-8aec-0be25e69aa2a/sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i
programhash 8f5e55a4b7a22c3d7de3d0a49a2ff34f668b1e90
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/5cf0008d584127d4e820147838bde31e93b56f6bd1f253fb130be9ff756107d7.graphml
witness-sha256 5cf0008d584127d4e820147838bde31e93b56f6bd1f253fb130be9ff756107d7
witness-size 787
witness-type violation_witness

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

Trying to find witnesses for program (24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120, sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i).

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

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

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

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

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

Found 24 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7c4d33b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2018-12-08T07:42 CET (sv-comp)
Download 47da1ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T04:55:04
Download 85593a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 23 2018-12-07T01:58 CET (sv-comp)
Download 5d7a56c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 8 2018-12-10T18:09:33+01:00
Download a767de1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-06T23:57:03+01:00
Download b4d94d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T20:35:49+01:00 Download 5d7a56c
Download ac7af54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T21:23:34+01:00 Download c614509
Download c469b4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:53:05+01:00 Download f2bd11d
Download 4796f86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:39:11+01:00 Download c78053c
Download 02f4e8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:16:47+01:00 Download c536499
Download a9e7bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1274 2018-12-09T17:57:01+01:00 Download 03ce82e
Download a4741d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1274 2018-12-08T23:44:56+01:00 Download 7c4d33b
Download 0f75b88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T22:11:09+01:00 Download 47da1ff
Download 79ec0e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T09:05:45+01:00 Download a767de1
Download 5c0e3ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:02:25+01:00 Download 948fd31
Download b75f99e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T18:48:02+01:00 Download 8a41009
Download 2278a3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T17:44:37+01:00 Download 85593a7
Download e289085 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:12:17+01:00 Download 899e8e3
Download 42ed053 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:48:56+01:00 Download b9e80e9
Download e1e0833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:10:31+01:00 Download ccb6cbd
Download b9e80e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T02:17:02+01:00
Download d0fc341 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:40:49+01:00 Download 88870c9
Download 41b1dcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:00:48+01:00 Download 7896e6f
Download 395447d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:33 CET (sv-comp)

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

Trying to find witnesses for program (24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120, sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i).

Found 20 witnesses for program sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i, 24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84accc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:27 CET (sv-comp)
Download b18a7da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 9 2017-12-03T00:23Z
Download 5cf0008 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T14:32 CET (sv-comp)
Download 25794ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 9 2017-12-02T17:17Z
Download 8ac003d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T04:45:52.622923
Download 196502b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T20:14:46.281240
Download ce8952c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T19:34 CET (sv-comp)
Download 3303da3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-11-30T21:55 CET (sv-comp)
Download 5168ded Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 9 2017-12-02T21:05:08+01:00
Download 96621b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 8 2017-11-30T19:26:01+01:00
Download b2ef604 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T21:57:06+01:00
Download ffd8668 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T20:03:22+01:00
Download 7d1a59b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-01T23:05:02+01:00
Download 00d48a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 28 2017-11-30T17:56 CET (sv-comp)
Download a4e6dd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 9 2017-12-02T10:25Z
Download 1c7ccbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 7 2017-11-30T22:47 CET (sv-comp)
Download 57a29dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:53:23.934407
Download 5bb1655 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:06:53.221269
Download 3a07626 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 938 2017-12-01T14:39 CET (sv-comp)
Download 51c5681 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 14 2017-12-01T15:48 CET (sv-comp)

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

Trying to find witnesses for program (24fdee424358788c80e2826508d31cf3d3a3871993c9b6c31ee6b12c8d2d2120, sv-benchmarks/c/loops/nec20_false-unreach-call_true-termination.i).

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

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