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/array-examples/sanfoundry_10_true-unreach-call_ground.i
programSHA 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
witnessName results-verified/viap.2018-12-09_1849.logfiles/sv-comp19_prop-reachsafety.sanfoundry_10_true-unreach-call_ground.i.files/witness.graphml
witnessSHA 3e3920df9ec8e67364717463ff8f5b81c30a3842338803b937331792b939b509

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T20:02 CET (sv-comp)
memorymodel precise
producer VIAP
programfile ../../sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i
programhash a5737e188310da8385da3f41be1e469dc9ec3023
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3e3920df9ec8e67364717463ff8f5b81c30a3842338803b937331792b939b509.graphml
witness-sha256 3e3920df9ec8e67364717463ff8f5b81c30a3842338803b937331792b939b509
witness-size 3565
witness-type correctness_witness

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

Trying to find witnesses for program (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.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 (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.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 (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.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 (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.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 (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.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 (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 9 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8548f2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T05:06 CET (sv-comp)
Download 906e534 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:00:48
Download 59c2b35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:30:19+01:00 Download 893b557
Download 6fe1520 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:21:25+01:00 Download 3e3920d
Download 02f2a47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:31:05+01:00 Download 8548f2a
Download 28d8390 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T22:00:40+01:00 Download 906e534
Download 898c872 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:19:24+01:00 Download 6c55b23
Download 6421b30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:00:08+01:00 Download d156d13
Download d156d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 23 2018-12-05T19:10:25+01:00

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

Trying to find witnesses for program (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 4 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8e4deaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T20:05 CET (sv-comp)
Download 3aee126 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download 6d2a48f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T04:18:48+01:00 83bb7e7
Download 9071235 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T22:20:43+01:00 6463c27

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

Trying to find witnesses for program (6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff, sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/sanfoundry_10_true-unreach-call_ground.i, 6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6012dc4b33d194a239f3c1f10d358af4e15cd6876b3208c83ffd219d903d89ff.json

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