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/n.c11_true-unreach-call_false-termination.i
programSHA d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6
witnessName results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.n.c11_true-unreach-call_false-termination.i.files/witness.graphml
witnessSHA f83b6df0eaab0a8b9070dcc5ea701be0a95afe1f67c81436d884d23028f29657

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T14:27:11+01:00
producer CPAchecker 1.6.1-svn 26758M
program-sha256 d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6
programfile ../../sv-benchmarks/c/loops/n.c11_true-unreach-call_false-termination.i
programhash 24b22c477e8a47eac290a2fc1c5b1e1aaa3a4fa4
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/f83b6df0eaab0a8b9070dcc5ea701be0a95afe1f67c81436d884d23028f29657.graphml
witness-sha256 f83b6df0eaab0a8b9070dcc5ea701be0a95afe1f67c81436d884d23028f29657
witness-size 10474
witness-type correctness_witness

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

Trying to find witnesses for program (d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6, sv-benchmarks/c/loops/n.c11_true-unreach-call_false-termination.i).

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

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

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

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

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

Found 11 witnesses for program sv-benchmarks/c/loops/n.c11_true-unreach-call_false-termination.i, d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c0144e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-07T19:32:26
Download eda448e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-07T01:18:03+01:00
Download 23e6d59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T19:55:26+01:00 Download 1351c85
Download 3818c62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:29:36+01:00 Download dad8e3f
Download a9514fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T19:50:17+01:00 Download c4ef71d
Download 1673428 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T17:28:43+01:00 Download d18dba6
Download 3a178ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T21:45:01+01:00 Download c0144e8
Download 18e05d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T07:01:11+01:00 Download eda448e
Download 66ddc5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T17:58:16+01:00 Download 31d0d05
Download 04d7ec8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:14:49+01:00 Download 003634e
Download 003634e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:35:07+01:00

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

Trying to find witnesses for program (d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6, sv-benchmarks/c/loops/n.c11_true-unreach-call_false-termination.i).

Found 15 witnesses for program sv-benchmarks/c/loops/n.c11_true-unreach-call_false-termination.i, d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 31d0d05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:31 CET (sv-comp)
Download eb7d21d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 7 2017-12-02T22:33Z
Download 30df5f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 7 2017-12-02T10:27Z
Download 3c72d17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T06:57:39+01:00 a33a817
Download 13e7d2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T04:18:57+01:00 c4656f3
Download 75a8782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T02:23:17+01:00 702db60
Download f8161da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T00:31:47+01:00 4360447
Download 8775858 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T15:17:51+01:00 32a86e6
Download 73d2fd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T07:00:34+01:00 61bc108
Download b297fbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T19:27:31+01:00
Download f83b6df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T14:27:11+01:00
Download 5d56b4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T23:59:31+01:00
Download e113c1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 6 2017-12-01T22:17:06+01:00
Download 79a580b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 7 2017-12-02T08:56Z
Download c1db203 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 10 2017-12-01T12:39 CET (sv-comp)

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

Trying to find witnesses for program (d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6, sv-benchmarks/c/loops/n.c11_true-unreach-call_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/n.c11_true-unreach-call_false-termination.i, d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d4b26dc59ca00b74a0c8b5a8e9bc414405fc413ee352539264683a47408a51a6.json

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