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 ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i
programSHA 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
witnessName results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.standard_copyInitSum3_true-unreach-call_ground.i.files/witness.graphml
witnessSHA a996925685b414c15c9766b6817e400641649188404f8637b3138b50dee268f9

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T21:16 CET (sv-comp)
producer Map2Check
program-sha256 2e7b0abb3d4463d645e542108ca2e28c55e1785d177d0007471b453c14e1a852
programfile ../../sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i
programhash 2c00e95d73976206e59c526d83b089135cd1a7ba
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a996925685b414c15c9766b6817e400641649188404f8637b3138b50dee268f9.graphml
witness-sha256 a996925685b414c15c9766b6817e400641649188404f8637b3138b50dee268f9
witness-size 4515
witness-type correctness_witness

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

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

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 5 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 8 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 6 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/array-examples/standard_copyInitSum3_true-unreach-call_ground.i).

Found 0 witnesses for program ../../../comp/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