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

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T17:44:07+01:00
producer CPAchecker 1.6.1-svn 26758M
program-sha256 f42d55abc7f560fa08e8c1d90fb5e53fa0a7f57ac2d6929c9f60b93362898d4f
programfile ../../sv-benchmarks/c/loops/for_infinite_loop_2_true-unreach-call_false-termination.i
programhash 26479c976733891620a412c0502cdbc3992d9719
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ddfa58e45d4dac99ffcf854fdf9e2af065920e5e2aaf3697ecbd4a8f98dcd6e4.graphml
witness-sha256 ddfa58e45d4dac99ffcf854fdf9e2af065920e5e2aaf3697ecbd4a8f98dcd6e4
witness-size 7508
witness-type correctness_witness

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

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

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

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/loops/for_infinite_loop_2_true-unreach-call_false-termination.i, f42d55abc7f560fa08e8c1d90fb5e53fa0a7f57ac2d6929c9f60b93362898d4f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f42d55abc7f560fa08e8c1d90fb5e53fa0a7f57ac2d6929c9f60b93362898d4f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 69df221 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T13:09:21
Download efb8ef7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-06T22:46:44+01:00
Download 7e68879 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:15:14+01:00 Download 570a8be
Download c645123 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:19:41+01:00 Download cdf5d49
Download 6d1ceaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:52:55+01:00 Download fe52e82
Download 51def76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:32:45+01:00 Download 27e620c
Download 777b807 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:42:08+01:00 Download 69df221
Download 7d551ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T06:15:41+01:00 Download efb8ef7
Download 297b3b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:43:20+01:00 Download 5f8e93a
Download 71d5444 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:32+01:00 Download c2b9cf2
Download 8ccac96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:59:52+01:00 Download 2981e82
Download 7464e7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:52:25+01:00 Download f60026c
Download 2981e82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T10:18:32+01:00

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

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

Found 22 witnesses for program sv-benchmarks/c/loops/for_infinite_loop_2_true-unreach-call_false-termination.i, f42d55abc7f560fa08e8c1d90fb5e53fa0a7f57ac2d6929c9f60b93362898d4f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f42d55abc7f560fa08e8c1d90fb5e53fa0a7f57ac2d6929c9f60b93362898d4f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5f8e93a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:04 CET (sv-comp)
Download 48d7c58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 7 2017-12-02T23:55Z
Download 73bb2b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 7 2017-12-02T14:29Z
Download 97ab845 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T20:53 CET (sv-comp)
Download 95301ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-12-03T03:09:48+01:00
Download 4b94edc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T07:03:49+01:00 a283f71
Download 0866ac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:20:57+01:00 b33c133
Download a0353f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:59:02+01:00 8742b77
Download a28e0bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:51:41+01:00 a88ed29
Download 9a41f97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T14:43:11+01:00 d0ccb31
Download 065082b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:16:18+01:00 f15735d
Download c6f839c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:27:12+01:00 d82b879
Download 3e68794 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:08:46+01:00 0641a83
Download a6a0419 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:40:36+01:00 0c78291
Download 3149282 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:14:05+01:00 9ae514e
Download c943c9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T18:51:40+01:00
Download ddfa58e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 8 2017-11-30T17:44:07+01:00
Download 8d8c5e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T14:05:08+01:00
Download 1f25d70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 6 2017-12-02T13:04:12+01:00
Download a9325a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 7 2017-12-02T00:45Z
Download b58ac0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 13 2017-12-01T02:59 CET (sv-comp)
Download f4e90e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 6 2017-12-03T11:18Z

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

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

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

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