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/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c
programSHA c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
witnessName results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c.files/witness.graphml
witnessSHA 1eeb9868588f47882fe461c76b04b13b4baec4400e0204d8c366eddad0b07358

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T07:49:56.426103
producer ESBMC 4.6.0 incr
program-sha256 c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
programfile ../../sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c
programhash f3d619d2c1c3b5319c1ba41a41e084c9947cb440
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/1eeb9868588f47882fe461c76b04b13b4baec4400e0204d8c366eddad0b07358.graphml
witness-sha256 1eeb9868588f47882fe461c76b04b13b4baec4400e0204d8c366eddad0b07358
witness-size 4209
witness-type violation_witness

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

Trying to find witnesses for program (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.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 (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.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 (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.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 (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.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 (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 15 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7b8f212 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 03:08:28
Download 4735004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:43:34+01:00 Download 651a987
Download 682a2b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T21:41:36+01:00 Download 310ab7d
Download 943c14e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:09:39+01:00 Download 7b8f212
Download 7c4a1c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:44:29+01:00 Download f706acd
Download 9f8cb86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:27:24+01:00 Download 9759263
Download 608b86f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T21:17:36+01:00 Download 71478f1
Download 9e4ad8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-06T02:38:03+01:00 Download f11c2e3
Download 9ec3083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T20:20:12+01:00 Download be2cfdb
Download 63f3aef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-03T08:56:50+01:00 Download ac3c4c3
Download e332c54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-03T08:08:12+01:00 Download 57a9dae
Download 57a9dae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 8 2019-11-29T14:19:00+01:00
Download 310ab7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 8 2019-11-30T20:56:34+01:00
Download 979ab75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:54:50+01:00 Download e0faffd
Download 0f6b359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T01:51:36+01:00 Download b6d12bd

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

Trying to find witnesses for program (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 25 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fc4ba99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T17:41:14
Download 3b34d5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 3084 2018-12-05T14:04:31+01:00
Download 262c19a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T01:39 CET (sv-comp)
Download c49659d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-07T19:17:45
Download d50fe4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2018-12-07T09:52 CET (sv-comp)
Download 6bb4b81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T21:43:36+01:00
Download a7def8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T21:23:29+01:00 Download 95a53aa
Download 739e01a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:08+01:00 Download 611aa76
Download 7298851 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:33:46+01:00 Download 5464879
Download 21715a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:33:44+01:00 Download d30fe11
Download 1863009 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T18:16:59+01:00 Download d59b423
Download c129845 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:44:14+01:00 Download 262c19a
Download 4063176 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T22:11:05+01:00 Download c49659d
Download c1e899a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T08:01:30+01:00 Download 6bb4b81
Download b24df10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:01:36+01:00 Download 3aac6d8
Download b287cbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:48:21+01:00 Download b24e213
Download 81dceb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T18:46:51+01:00 Download e52f830
Download 0a6773d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T17:08:01+01:00 Download d50fe4e
Download 0e3177a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T01:23:38+01:00 Download 6230c36
Download 95f8bfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:20:02+01:00 Download 367ecf3
Download 3dd1d03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:48:51+01:00 Download b2d0bc5
Download e2fc868 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:17:39+01:00 Download a13e9d5
Download 3b22e41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:12:33+01:00 Download 38975ec
Download b2d0bc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T07:33:41+01:00
Download 3c6a5f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:36:33+01:00 Download 9bb35bb

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

Trying to find witnesses for program (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 384ca48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 12 2017-12-03T07:44Z
Download ee9d89d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 12 2017-12-03T10:24Z
Download ff393f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:36 CET (sv-comp)
Download 9fd9fd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 6 Sat Dec 2 20:45:04 2017
Download eb2cd8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 6 2017-12-03T01:34Z
Download a76bf4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T12:34 CET (sv-comp)
Download 55f20c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:37 CET (sv-comp)
Download 1463fce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 6 2017-12-02T12:59Z
Download 5555af5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T22:44:50.890750
Download 1eeb986 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T07:49:56.426103
Download 4f50f1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T20:15 CET (sv-comp)
Download 4222dbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T05:17 CET (sv-comp)
Download ba12c00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 8 2017-11-30T21:11:09+01:00
Download 2089b90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 14 2017-11-30T15:19:48+01:00
Download 508215b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T16:11:05+01:00
Download b00953b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 8 2017-12-02T09:09:36+01:00
Download 1d4d249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 5 2017-11-30T21:41 CET (sv-comp)
Download 3d4071c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T18:54Z

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

Trying to find witnesses for program (c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6, sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c, c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c2d9227835ffc2c4a68881fb2a6827cc211039c2af4b032c349d86494bbca0b6.json

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