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/floats-cdfpl/square_1_false-unreach-call_true-termination.i
programSHA 685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c
witnessName results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-reachsafety.square_1_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 114866c39d439b04bc5adbe59d26dc52e54d14d19b26cba55df21f4f0f4caeaa

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/114866c39d439b04bc5adbe59d26dc52e54d14d19b26cba55df21f4f0f4caeaa.json

Key Value
architecture 32bit
creationtime 2018-12-05T12:03 CET (sv-comp)
producer 2LS
programfile ../../sv-benchmarks/c/floats-cdfpl/square_1_false-unreach-call_true-termination.i
programhash 9b4984d971b5a5a3b565edf502e7d7464558f166
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/114866c39d439b04bc5adbe59d26dc52e54d14d19b26cba55df21f4f0f4caeaa.graphml
witness-sha256 114866c39d439b04bc5adbe59d26dc52e54d14d19b26cba55df21f4f0f4caeaa
witness-size 4197
witness-type violation_witness

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

Trying to find witnesses for program (685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c, sv-benchmarks/c/floats-cdfpl/square_1_false-unreach-call_true-termination.i).

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

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

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

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

Found 19 witnesses for program sv-benchmarks/c/floats-cdfpl/square_1_false-unreach-call_true-termination.i, 685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84ac282 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-03T22:06 CET (comp)
Download e08b3d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:42:50+01:00 Download 27a8190
Download c667567 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:51:34+01:00 Download d884342
Download 447d1a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:57:10+01:00 Download e6d7a35
Download 8b63956 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:09:48+01:00 Download 7354a9c
Download 7354a9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T07:39:59+01:00
Download d884342 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 4 2019-12-07T10:20:09+01:00
Download 27a8190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T01:52:53+01:00
Download 848fef6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness BRICK 4 2019-12-07T21:38:56Z
Download d3bcb8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T21:09:11+01:00 Download 47fb0b7
Download df26d7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:54:45+01:00 Download 84f2e61
Download 8e4f538 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:44:52+01:00 Download 62d8bd4
Download f9c4e1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:26:39+01:00 Download 573731d
Download 7de753b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:51:25+01:00 Download 848fef6
Download 42c27a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T21:17:56+01:00 Download 25b37a3
Download e493b2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T20:20:40+01:00 Download 5a4176f
Download ae14eca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:34:03+01:00 Download 5a16db2
Download af054c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:58:25+01:00 Download 84ac282
Download 238ab4e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:38 CET (comp)

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

Trying to find witnesses for program (685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c, sv-benchmarks/c/floats-cdfpl/square_1_false-unreach-call_true-termination.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 13c674c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T05:12:53
Download 6949d79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-06T21:31 CET (sv-comp)
Download 981963e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 4 2018-12-10T17:25:40+01:00
Download c91d262 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T10:20:50+01:00
Download c7197b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:37:03+01:00 Download 981963e
Download 77b3fc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:16+01:00 Download 7f72a96
Download c115623 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:38:39+01:00 Download 727ad7a
Download 63f8e40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T18:22:17+01:00 Download 2418297
Download 606747a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T08:24:52+01:00 Download c91d262
Download bbc5432 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 eb663bd
Download 2945dda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:41:52+01:00 Download 114866c
Download 4be623b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:16:56+01:00 Download c15282f
Download eb663bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T20:11:35+01:00
Download 8d51e87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:05:51+01:00 Download 2e7ec90
Download b7fc75d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:44:57+01:00 Download 6949d79
Download f54d198 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T10:19:00+01:00 Download 4568516
Download 08903ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:18:14+01:00 Download 4ab9452
Download 94ae665 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T08:09 CET (sv-comp)

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

Trying to find witnesses for program (685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c, sv-benchmarks/c/floats-cdfpl/square_1_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/floats-cdfpl/square_1_false-unreach-call_true-termination.i, 685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 28d0afc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:08 CET (sv-comp)
Download 522e3df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-02T21:10Z
Download 0effb74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T13:52:57.465153
Download bdefb95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T20:07:46.949023
Download e390be7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T20:37 CET (sv-comp)
Download 1a16803 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T02:30 CET (sv-comp)
Download cf2dc08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-03T01:56:35+01:00
Download 9763d08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T17:09:48+01:00
Download db1b40a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T13:08:47+01:00
Download a59bcbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T22:45:46+01:00
Download d0d0144 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T23:24:54+01:00
Download 9de8fa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T18:48 CET (sv-comp)
Download eeea48a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T19:08Z
Download d827f46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-12-01T01:03 CET (sv-comp)
Download ba57f7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:56:07.196069
Download b0d004e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:35:56.888595
Download ef4f7ab Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T14:52 CET (sv-comp)
Download 158c6e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T11:50 CET (sv-comp)

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

Trying to find witnesses for program (685f9b20c614008fb68f733f5d90a8847cd3bfb2935e37a8b0fe39b7a98eea0c, sv-benchmarks/c/floats-cdfpl/square_1_false-unreach-call_true-termination.i).

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

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