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_copy1_false-unreach-call_ground.i
programSHA 60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.standard_copy1_false-unreach-call_ground.i.files/witness.graphml
witnessSHA 77bea56df9b621915adc14e6397f7b1786bc63def687260afdfda19356c14192

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T18:27 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac
programfile /tmp/vcloud-vcloud-master/worker/working_dir_f87e950b-05d1-4b1c-97ea-35577caaf984/sv-benchmarks/c/array-examples/standard_copy1_false-unreach-call_ground.i
programhash 0934b6a35c18e3b1129f1d4a76858d26412270b9
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/77bea56df9b621915adc14e6397f7b1786bc63def687260afdfda19356c14192.graphml
witness-sha256 77bea56df9b621915adc14e6397f7b1786bc63def687260afdfda19356c14192
witness-size 8158
witness-type correctness_witness

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

Trying to find witnesses for program (60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac, sv-benchmarks/c/array-examples/standard_copy1_false-unreach-call_ground.i).

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

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

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

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

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

Found 3 witnesses for program sv-benchmarks/c/array-examples/standard_copy1_false-unreach-call_ground.i, 60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 233cd63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T00:32 CET (sv-comp)
Download fa31af2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T03:45:41
Download e8a5406 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 170199 2018-12-07T01:48 CET (sv-comp)

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

Trying to find witnesses for program (60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac, sv-benchmarks/c/array-examples/standard_copy1_false-unreach-call_ground.i).

Found 5 witnesses for program sv-benchmarks/c/array-examples/standard_copy1_false-unreach-call_ground.i, 60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fba4374 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 22347 Sun Dec 3 02:36:51 2017
Download aff1525 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 4 2017-12-03T03:48 CET (sv-comp)
Download 8aa7f8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T10:48 CET (sv-comp)
Download 77bea56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-11-30T18:27 CET (sv-comp)
Download 317e798 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:37:45+01:00 71f3734

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

Trying to find witnesses for program (60ef6002ca223d6358817895ec4f8e677799354be7ccbaed39511102ad0a90ac, sv-benchmarks/c/array-examples/standard_copy1_false-unreach-call_ground.i).

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

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