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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.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 (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.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 (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.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 (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.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 (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 17 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a3a0958 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-03T22:22 CET (comp)
Download a53c054 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:41:24+01:00 Download c9537ce
Download d3f4337 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:06:12+01:00 Download 60e0f61
Download 60e0f61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-29T14:44:23+01:00
Download c9537ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-11-30T21:24:50+01:00
Download bad760d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness BRICK 4 2019-12-07T21:37:11Z
Download 55cc98e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T21:09:00+01:00 Download e3f67df
Download 3d8c74c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:55:03+01:00 Download f3497b3
Download df3e70f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:44:27+01:00 Download 8e2cccb
Download a89a716 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T01:51:46+01:00 Download afb3ba3
Download 877f601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:26:41+01:00 Download 4dd38d5
Download b5307f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:51:23+01:00 Download bad760d
Download cbd1596 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T21:15:29+01:00 Download f62afdc
Download d7c7037 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T20:20:51+01:00 Download 5e1eab7
Download 34c7f3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:34:37+01:00 Download 516a5d1
Download 2af4ef4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:58:20+01:00 Download a3a0958
Download fe72ad5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:34 CET (comp)

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

Trying to find witnesses for program (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bebbcb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T12:56:26
Download 20fb2f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-07T02:55 CET (sv-comp)
Download 98b6250 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 4 2018-12-10T18:00:30+01:00
Download 15bba82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T17:09:53+01:00
Download f107e33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:39:37+01:00 Download 98b6250
Download 7c3fedb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:49+01:00 Download 2f6da49
Download eb813af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:38:26+01:00 Download c727044
Download eddbac1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T08:27:40+01:00 Download 15bba82
Download 3760c16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:48:46+01:00 Download 1860886
Download e2cd17e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:41:20+01:00 Download 6428272
Download 0df6e7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:07:59+01:00 Download 869ab71
Download 1860886 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T05:53:20+01:00
Download c43e4fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T18:01:13+01:00 Download a685c05
Download 7e73bf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:52:56+01:00 Download 292f3ea
Download ef7e8ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:44:58+01:00 Download 20fb2f7
Download 115ffe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T10:18:33+01:00 Download 3f975f0
Download 42e438f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:20:00+01:00 Download 3d69ad9
Download fe9437e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:45 CET (sv-comp)

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

Trying to find witnesses for program (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 44e68ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:29 CET (sv-comp)
Download 7e53455 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-03T05:04Z
Download 5e8ecd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T22:08:00.541737
Download 6d4ef8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T08:05:10.547587
Download beb55a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-03T01:27:04+01:00
Download 75f34ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T17:48:12+01:00
Download d791511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T23:20:26+01:00
Download 2643db0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T16:05:21+01:00
Download b29fd6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T00:31:31+01:00
Download 5de4ab4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T12:20 CET (sv-comp)
Download b786701 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T03:33Z
Download abfc73d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T13:07 CET (sv-comp)
Download b604c17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:59:46.899001
Download e7e6996 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T07:55:15.335348
Download 863e24d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T16:31 CET (sv-comp)
Download c1e8243 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T12:57 CET (sv-comp)

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

Trying to find witnesses for program (04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68, sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/square_2_false-unreach-call_true-termination.i, 04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/04e99898e7c14ca8d4788c1ee6dfb8cfc10e4bc5e080d3bec1552f2725057b68.json

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