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_label04_false-unreach-call.c
programSHA 8fd213950d707fa2d76a19c11317f9a8a9cfce2f87b0468b39cf6e2303cacf78
witnessName results-verified/verifuzz.2018-12-09_0247.logfiles/sv-comp19_prop-reachsafety.Problem06_label04_false-unreach-call.c.files/witness.graphml
witnessSHA 1a1af7e886838ad033c04bc64d460a83885782abd4628217fba5777d9244e036

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/1a1af7e886838ad033c04bc64d460a83885782abd4628217fba5777d9244e036.json

Key Value
architecture 32bit
creationtime 2018-12-09T13:12 CET (sv-comp)
memorymodel precise
producer verifuzz
programfile /home/benchexec/VERIFUZZ_TEMP_DIR/OUT/Problem06_label04_false-unreach-call.c
programhash aff400803fb3df677fa7e8d42374ec634e11ab41
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/1a1af7e886838ad033c04bc64d460a83885782abd4628217fba5777d9244e036.graphml
witness-sha256 1a1af7e886838ad033c04bc64d460a83885782abd4628217fba5777d9244e036
witness-size 3441
witness-type violation_witness

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

Trying to find witnesses for program (8fd213950d707fa2d76a19c11317f9a8a9cfce2f87b0468b39cf6e2303cacf78, sv-benchmarks/c/eca-rers2012/Problem06_label04_false-unreach-call.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2b6a36e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 16:09:15
Download d6429f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 682 2019-12-04T00:17 CET (comp)
Download 47dfe36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2404 2019-12-11T21:58:19+01:00 Download 855a37a
Download 246c269 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2403 2019-12-11T21:09:32+01:00 Download 2b6a36e
Download bb8dd2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2404 2019-12-11T20:55:02+01:00 Download 23db8ac
Download c3d91bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2404 2019-12-11T20:44:38+01:00 Download 9a7093e
Download 9be0c7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 3218 2019-12-04T02:58:38+01:00 Download d6429f8
Download 46b4366 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2404 2019-12-03T08:10:06+01:00 Download e7a1db4
Download e7a1db4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 2447 2019-11-30T09:22:10+01:00
Download 855a37a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 2433 2019-12-01T01:51:21+01:00

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

Trying to find witnesses for program (8fd213950d707fa2d76a19c11317f9a8a9cfce2f87b0468b39cf6e2303cacf78, sv-benchmarks/c/eca-rers2012/Problem06_label04_false-unreach-call.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9beda09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-07T23:57 CET (sv-comp)
Download e4f9b69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 740 2018-12-07T07:49 CET (sv-comp)
Download 10db7c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 2447 2018-12-07T00:04:06+01:00
Download 0c0a746 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2404 2018-12-09T17:57:53+01:00 Download 1a1af7e
Download 5d47c6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2432 2018-12-08T23:45:27+01:00 Download 9beda09
Download f7356b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2404 2018-12-08T08:28:53+01:00 Download 10db7c2
Download ab72bd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2404 2018-12-08T04:56:26+01:00 Download e6a5fd1
Download 2228744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 3218 2018-12-07T17:38:18+01:00 Download e4f9b69
Download 6a4ad68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2403 2018-12-06T10:16:26+01:00 Download e1cb3ba
Download 21cc264 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2404 2018-12-06T09:48:10+01:00 Download 6ad3848
Download 596d91b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 3219 2018-12-06T09:14:43+01:00 Download 15a56cb
Download 6ad3848 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 2447 2018-12-06T05:37:23+01:00

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

Trying to find witnesses for program (8fd213950d707fa2d76a19c11317f9a8a9cfce2f87b0468b39cf6e2303cacf78, sv-benchmarks/c/eca-rers2012/Problem06_label04_false-unreach-call.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b330c56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T15:50 CET (sv-comp)
Download d986343 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T13:07:23.101502
Download df3c115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T09:58:41.792097
Download 52b075f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 1359 2017-11-30T12:55:31+01:00
Download dbafaf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 846 2017-11-30T12:17 CET (sv-comp)

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

Trying to find witnesses for program (8fd213950d707fa2d76a19c11317f9a8a9cfce2f87b0468b39cf6e2303cacf78, sv-benchmarks/c/eca-rers2012/Problem06_label04_false-unreach-call.c).

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

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