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/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c
programSHA 243bad48d0f0dc066785e00be186963d948e6b8b3d32c98b1f6c6bef2a72270b
witnessName results-verified/uautomizer.2017-12-03_1117.logfiles/sv-comp18.EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c.files/witness.graphml
witnessSHA df7c02219ba59a635d219380476f371ecb6d358c9ac84d08930ff5134e2d31db

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-03T10:27Z
producer Automizer
program-sha256 243bad48d0f0dc066785e00be186963d948e6b8b3d32c98b1f6c6bef2a72270b
programfile /tmp/vcloud-vcloud-master/worker/working_dir_588b051b-718e-4ead-8f39-41dca8fc3ac5/sv-benchmarks/c/recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c
programhash bec5669c6fe02e51518958076fea4487ada345cf
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/df7c02219ba59a635d219380476f371ecb6d358c9ac84d08930ff5134e2d31db.graphml
witness-sha256 df7c02219ba59a635d219380476f371ecb6d358c9ac84d08930ff5134e2d31db
witness-size 11622
witness-type correctness_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d4acfa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:36:34+01:00 Download 80fd5c2
Download 4c9cd05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-11-30T17:26:23+01:00 Download be644f0
Download be644f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 231 2019-11-29T17:16:41+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 38272ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:54:48
Download cc20f39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 3084 2018-12-06T00:42:03+01:00
Download 5bd2d90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T13:16:49
Download 00b8e45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 282 2018-12-06T21:46:09+01:00
Download 80a59b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:06:36+01:00 Download 698baf0
Download f617b2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T21:42:30+01:00 Download 5bd2d90
Download eab26dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T05:23:40+01:00 Download 00b8e45
Download fee1b2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:28:15+01:00 Download 00d57e2
Download 9e8d19b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T08:53:38+01:00 Download 4070f97
Download 4070f97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 296 2018-12-05T20:26:10+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ccbcb35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 12 2017-12-03T07:43Z
Download df7c022 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 12 2017-12-03T10:27Z
Download 8773e76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 14 2017-11-30T23:19:35+01:00
Download 6635385 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-12-01T03:06:48+01:00
Download 0a13ddb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 8 2017-12-02T12:06:18+01:00
Download 2f98c8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-01T23:24 CET (sv-comp)
Download 0486176 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T19:08 CET (sv-comp)
Download 6e3d2a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 9 2017-11-30T23:12:35+01:00
Download e350a54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T20:17:47+01:00 ec92d0e
Download 56748fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T08:14:05+01:00 162d95c

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

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

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

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