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/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c
programSHA ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
witnessName results-verified/verifuzz.2018-12-09_0247.logfiles/sv-comp19_prop-reachsafety.pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c.files/witness.graphml
witnessSHA 8df210c25a2d8c592ce3edb02798e5d1a246608eef7c753a5267d1f810294587

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/8df210c25a2d8c592ce3edb02798e5d1a246608eef7c753a5267d1f810294587.json

Key Value
architecture 32bit
creationtime 2018-12-09T08:10 CET (sv-comp)
memorymodel precise
producer verifuzz
programfile /home/benchexec/VERIFUZZ_TEMP_DIR/OUT/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c
programhash d5e0d3ca9e7124b9bb53333ae26103ee15477513
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/8df210c25a2d8c592ce3edb02798e5d1a246608eef7c753a5267d1f810294587.graphml
witness-sha256 8df210c25a2d8c592ce3edb02798e5d1a246608eef7c753a5267d1f810294587
witness-size 11758
witness-type violation_witness

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

Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.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 (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 10 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 71166cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T21:42:58+01:00 Download 2aacadd
Download 3c26c89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 315 2019-12-11T20:44:29+01:00 Download ed35c00
Download 5643a70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 315 2019-12-08T01:51:18+01:00 Download b4dec37
Download 1d02d48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 316 2019-12-03T08:00:48+01:00 Download f67b4dc
Download f67b4dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 322 2019-11-29T18:17:02+01:00
Download b4dec37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 254 2019-12-07T20:31:06+01:00
Download 2aacadd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 281 2019-12-01T09:54:23+01:00
Download 4403ed9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 126 2019-12-11T20:54:56+01:00 Download 6813c69
Download 0cf01c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 126 2019-12-05T20:20:45+01:00 Download 39249e8
Download 7b780f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 126 2019-12-05T19:34:30+01:00 Download 3f2bcb4

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

Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 71fa46a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 18 2018-12-08T04:52 CET (sv-comp)
Download 19226ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 76 2018-12-08T04:58:21
Download 4fd033a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 283 2018-12-07T23:38:18+01:00
Download ed8a0da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 315 2018-12-09T18:21:58+01:00 Download 8df210c
Download 08887e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 287 2018-12-08T23:44:52+01:00 Download 71fa46a
Download 30d48ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 287 2018-12-08T08:58:31+01:00 Download 4fd033a
Download 34a2fb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 289 2018-12-08T05:05:10+01:00 Download 515d8bc
Download 60731a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 289 2018-12-06T10:19:25+01:00 Download 3bf1481
Download 5e4e8a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 316 2018-12-06T09:48:08+01:00 Download ef85b91
Download ef85b91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 322 2018-12-05T17:55:00+01:00
Download 06d6517 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 126 2018-12-10T20:38:29+01:00 Download 11b6d27
Download 476930e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 126 2018-12-08T22:11:26+01:00 Download 19226ce
Download fa51207 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 126 2018-12-06T09:43:06+01:00 Download 2e369f7
Download 2b732b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 126 2018-12-06T09:16:03+01:00 Download 6e42d58

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

Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b687984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 243 Sat Dec 2 23:47:33 2017
Download bef3497 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 16 2017-12-01T23:36 CET (sv-comp)
Download b17d6b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 32 2017-12-01T19:45:44.306359
Download fd2289b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 35 2017-12-01T19:22:19.268648
Download 96446cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 94 2017-12-01T20:35 CET (sv-comp)
Download 973057d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 99 2017-11-30T16:17 CET (sv-comp)
Download db098dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 307 2017-11-30T12:27:33+01:00
Download 5d610e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 247 2017-11-30T11:42 CET (sv-comp)
Download 211eeb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 199 2017-11-30T18:04 CET (sv-comp)
Download 7acd1ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:22:06.622502
Download 4cbad51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:19:45.496819
Download 9639716 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 609 2017-12-01T17:47 CET (sv-comp)
Download 00a53ce Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 267 2017-12-01T15:01 CET (sv-comp)

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

Trying to find witnesses for program (ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c, ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ebcfc2636c039ce113df9bd4fa1f4a0e9e0d33e9c8dafec5242235f0c95c3d3d.json

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