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/standard_copyInitSum3_true-unreach-call_ground.i
programSHA 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
witnessName results-validated/cpa-seq-validate-correctness-witnesses-pinaka.2018-12-07_1617.logfiles/sv-comp19_prop-reachsafety.standard_copyInitSum3_true-unreach-call_ground.i.files/witness.graphml
witnessSHA 64ff63331ae926fff6fad3ff4301871fc1c58422be3589cd6a1fbdb7cfd9564c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T16:52:47+01:00
inputwitnesshash 5620583bf507d4a0315e92fd58c6da5642eeb3e5afbfbb96dd7dee7dfd9028e5
producer CPAchecker 1.7-svn 29852
program-sha256 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
programfile ../../sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i
programhash 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/64ff63331ae926fff6fad3ff4301871fc1c58422be3589cd6a1fbdb7cfd9564c.graphml
witness-sha256 64ff63331ae926fff6fad3ff4301871fc1c58422be3589cd6a1fbdb7cfd9564c
witness-size 8983
witness-type correctness_witness

This witness was created for this program (cf. table above, 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852).

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

Trying to find witnesses for program (2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852, sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

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

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

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

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

Found 5 witnesses for program sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i, 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fa4d725 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:16 CET (comp)
Download a5c1760 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:43:01+01:00 Download 4c7a810
Download 0b722ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T01:02:23+01:00 Download 36a3f28
Download 38cd1cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-06T02:26:29+01:00 Download 2ad90ca
Download b90bbcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-04T02:22:40+01:00 Download fa4d725

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

Trying to find witnesses for program (2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852, sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 8 witnesses for program sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i, 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bc5daa7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T06:30 CET (sv-comp)
Download 4f6fcbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:18:01
Download 5620583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T12:09 CET (sv-comp)
Download 8462d4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:08:59+01:00 Download 44ad3af
Download 03b9e08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:21:23+01:00 Download 5f3175b
Download dd968b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:28:33+01:00 Download bc5daa7
Download 4361df0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T21:55:49+01:00 Download 4f6fcbe
Download 64ff633 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T16:52:47+01:00 Download 5620583

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

Trying to find witnesses for program (2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852, sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 6 witnesses for program sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i, 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 267cc88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T18:51 CET (sv-comp)
Download a996925 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 5 2017-12-01T21:16 CET (sv-comp)
Download 357771f 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 e6fe6d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T04:42:56+01:00 d0b8453
Download 3f517b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T20:14:07+01:00 21ab9dc
Download 62058ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T22:27:18+01:00 43859ba

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

Trying to find witnesses for program (2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852, sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

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

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