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/eca-rers2012/Problem06_label59_false-unreach-call.c
programSHA d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
witnessName results-verified/veriabs.2018-12-10_1650.logfiles/sv-comp19_prop-reachsafety.Problem06_label59_false-unreach-call.c.files/witness.graphml
witnessSHA 82ff958e6033fb09afba9fca457cbe7734ac32bc9689f4af221a944c280b95c0

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T17:22 CET (sv-comp)
memorymodel precise
producer Veriabs
programfile /home/benchexec/ar_abs_temp/Problem06_label59_false_unreach_call_c.c
programhash 63b80953173c84318100b6fdf6e5040692c287ab
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/82ff958e6033fb09afba9fca457cbe7734ac32bc9689f4af221a944c280b95c0.graphml
witness-sha256 82ff958e6033fb09afba9fca457cbe7734ac32bc9689f4af221a944c280b95c0
witness-size 4633
witness-type violation_witness

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

Trying to find witnesses for program (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.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 (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.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 (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.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 (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.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 (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 10 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d2f2c91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-02 00:04:01
Download 704027e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 716 2019-12-03T23:19 CET (comp)
Download ed31c35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2527 2019-12-11T21:42:57+01:00 Download 6e3115d
Download 3eb89f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2527 2019-12-11T21:09:50+01:00 Download d2f2c91
Download cf722c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2527 2019-12-11T20:55:06+01:00 Download 876b151
Download 8af3854 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2527 2019-12-11T20:44:39+01:00 Download ce2b1a8
Download be1311b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 3384 2019-12-04T02:58:16+01:00 Download 704027e
Download 9e16315 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2527 2019-12-03T08:10:38+01:00 Download 4add50f
Download 4add50f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 2572 2019-11-30T07:40:54+01:00
Download 6e3115d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 2557 2019-12-01T02:18:13+01:00

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

Trying to find witnesses for program (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 99435d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T02:23 CET (sv-comp)
Download b86e939 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 776 2018-12-06T21:38 CET (sv-comp)
Download 04e8f43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 2572 2018-12-07T15:42:52+01:00
Download 21619ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2527 2018-12-09T18:21:40+01:00 Download 2977de7
Download 4017054 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2552 2018-12-08T23:45:28+01:00 Download 99435d8
Download e3f4b86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2527 2018-12-08T08:34:39+01:00 Download 04e8f43
Download 9de6815 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2527 2018-12-08T04:54:30+01:00 Download 5d3344e
Download 164b84e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 3384 2018-12-07T17:44:01+01:00 Download b86e939
Download 301f12c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2527 2018-12-06T10:18:56+01:00 Download d7d0760
Download d172d6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2527 2018-12-06T09:48:09+01:00 Download 0a95a69
Download 13da6fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 3384 2018-12-06T09:18:43+01:00 Download 4667fa4
Download 0a95a69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2572 2018-12-05T18:01:11+01:00

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

Trying to find witnesses for program (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fa744ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T14:14 CET (sv-comp)
Download 83abb00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T04:52:39.691921
Download 3908dd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T15:43:19.185300
Download 461d984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 1426 2017-12-01T01:17:40+01:00
Download 234ebfd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 887 2017-12-01T00:43 CET (sv-comp)

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

Trying to find witnesses for program (d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636, sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label59_false-unreach-call.c, d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d39cd58b531d314ccdbfdea6f3119fcd183f4a76f6da5aeaa94cc8c937d47636.json

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