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/trex03_true-unreach-call_true-termination.i
programSHA 07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef
witnessName results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.trex03_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA cc34eb8024560bf89a198a89635737f2b2f02202750a44eebec7706683f7aed0

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T05:38:08+01:00
producer CPAchecker 1.7-svn 29852
program-sha256 07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef
programfile ../../sv-benchmarks/c/loops/trex03_true-unreach-call_true-termination.i
programhash 07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/cc34eb8024560bf89a198a89635737f2b2f02202750a44eebec7706683f7aed0.graphml
witness-sha256 cc34eb8024560bf89a198a89635737f2b2f02202750a44eebec7706683f7aed0
witness-size 7788
witness-type correctness_witness

This witness was created for this program (cf. table above, 07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef).

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

Trying to find witnesses for program (07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef, sv-benchmarks/c/loops/trex03_true-unreach-call_true-termination.i).

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

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/loops/trex03_true-unreach-call_true-termination.i, 07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 01a5246 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:19:34
Download 4e28caa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-08T04:06:50+01:00
Download e6d78b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-10T19:47:43+01:00 Download 48e4aa1
Download a8900a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T21:06:41+01:00 Download a88813e
Download 512f24f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:20:45+01:00 Download 3d25084
Download fbdc20c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:07:14+01:00 Download 5d014ac
Download 8943f8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T19:52:09+01:00 Download 8f4d832
Download bc8d2dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T21:47:25+01:00 Download 01a5246
Download 388b8fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T06:21:15+01:00 Download 4e28caa
Download 1e2cbe9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:28:16+01:00 Download d97d1bb
Download 30a238c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:00:37+01:00 Download cc34eb8
Download 2bc6f7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T07:14:26+01:00 Download e22ea38
Download cc34eb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T05:38:08+01:00

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

Trying to find witnesses for program (07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef, sv-benchmarks/c/loops/trex03_true-unreach-call_true-termination.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 162880f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 9 2017-12-02T18:51Z
Download 3feae7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 9 2017-12-02T14:58Z
Download 34abf5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T20:19 CET (sv-comp)
Download 7684907 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 9 2017-12-02T21:07:48+01:00
Download 9cc539d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:30:46+01:00
Download 81c3e02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T06:51:34+01:00 3a58b7b
Download b233e0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T04:23:18+01:00 32deee5
Download 78ec5c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T00:45:47+01:00 ea36096
Download 412c35c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T23:55:38+01:00 8b94ff0
Download 6751eaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T15:12:13+01:00 12e0970
Download 96959cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T08:13:58+01:00 cd13887
Download 65eb447 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T06:43:04+01:00 252366b
Download 26163cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T05:49:25+01:00 3028f5e
Download f61fe25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T01:42:49+01:00
Download 7a2fe6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 8 2017-12-02T07:26:19+01:00
Download 19fe823 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 9 2017-12-02T06:08Z
Download 45cbac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 14 2017-11-30T21:56 CET (sv-comp)
Download 5a4882f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 14 2017-12-01T12:34 CET (sv-comp)

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

Trying to find witnesses for program (07100153b2e5ee2035b9fb2a13032e9b13d5fd539042ce4d8b66e3ed11458fef, sv-benchmarks/c/loops/trex03_true-unreach-call_true-termination.i).

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

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