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-cbmc-regression/float1_true-unreach-call_true-termination.i
programSHA 64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7
witnessName results-verified/skink.2018-12-07_1200.logfiles/sv-comp19_prop-reachsafety.float1_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 996b46ce61a19daf25995c1ffa028ae2893e6e182696f5d9c179165b94b05918

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/996b46ce61a19daf25995c1ffa028ae2893e6e182696f5d9c179165b94b05918.json

Key Value
architecture 32bit
creationtime 2018-12-07T15:52 CET (sv-comp)
memorymodel simple
producer skink
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i
programhash d83baf1cdb4ca03660244dae388672dd75d02b3f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/996b46ce61a19daf25995c1ffa028ae2893e6e182696f5d9c179165b94b05918.graphml
witness-sha256 996b46ce61a19daf25995c1ffa028ae2893e6e182696f5d9c179165b94b05918
witness-size 2612
witness-type correctness_witness

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

Trying to find witnesses for program (64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7, sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i).

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i, 64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7.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 '19

Trying to find witnesses for program (64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7, sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i).

Found 23 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i, 64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2eb56f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-07T23:06 CET (sv-comp)
Download af0fff9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:36:57
Download 6551587 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T07:04 CET (sv-comp)
Download 0788dd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-06T13:30:50+01:00
Download 024efde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T19:56:01+01:00 Download 1d838e4
Download 3dbbcf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:30:41+01:00 Download c7a1e3e
Download 9bbc166 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:15:25+01:00 Download eb56903
Download 385b679 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:40:53+01:00 Download f30c49a
Download a32beae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T17:13:23+01:00 Download e39a678
Download 09e3b9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:11:14+01:00 Download 2eb56f3
Download 2c09a1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:49:28+01:00 Download af0fff9
Download eab05d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:38:21+01:00 Download 0788dd2
Download cd88476 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T03:05:34+01:00 Download 32b0f1b
Download 97e74e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:04:06+01:00 Download c7a1e3e
Download d2314a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:45:17+01:00 Download 996b46c
Download 4a72bde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:37:19+01:00 Download 6551587
Download b433f5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:28:44+01:00 Download b6e97b6
Download 6e54aed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:45:25+01:00 Download d469c0d
Download ffa23ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:16:23+01:00 Download 0211cad
Download 5308283 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:57:17+01:00 Download d6be8d0
Download d469c0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T16:39:00+01:00
Download c360e29 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:10 CET (sv-comp)
Download b278192 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T21:33 CET (sv-comp)

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

Trying to find witnesses for program (64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7, sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i).

Found 34 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i, 64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c4b9f44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-02T08:03:07+01:00
Download 996b46c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:36 CET (sv-comp)
Download 3b7f4f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T02:48Z
Download b8a9869 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T16:37 CET (sv-comp)
Download 9bea7fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T09:01Z
Download 0391251 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:49:37.263988
Download 36d606d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:50:53.058809
Download 38ac53b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T22:37:29.508276
Download 521ee37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T20:07:24.715508
Download e3eed03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T15:35 CET (sv-comp)
Download b7f8888 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 3 2017-12-03T00:09:27+01:00
Download 7ab7f52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T22:12:31+01:00
Download 151381f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T06:50:41+01:00 a2c6298
Download d503604 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T03:57:56+01:00 5b5e4aa
Download 3c1edb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:53:44+01:00 ea532e7
Download 735e6ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T23:28:38+01:00 5ca6290
Download a38339e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:47:08+01:00 a1859a5
Download 27ebd61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T08:46:23+01:00 a0ba311
Download b8293e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:08:47+01:00 f82de97
Download 30d3f29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:22:10+01:00 2d3dff0
Download ed8572b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:56+01:00 7592488
Download 29ea409 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:04:32+01:00 3a7bc39
Download 73d705b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:42:38+01:00 59c6a70
Download 9e213c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:06:31+01:00 881cabd
Download 265f050 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:01:33+01:00 c4efb77
Download 1180179 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:18:38+01:00 b0db7ab
Download 776a283 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T02:34:02+01:00
Download 47158fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T17:38:07+01:00
Download 7c7a173 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T02:04:47+01:00
Download 38bdb6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 6 2017-12-01T02:39 CET (sv-comp)
Download 3979e61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T14:10Z
Download 357b43f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-11-30T23:38 CET (sv-comp)
Download 50377c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T18:10 CET (sv-comp)
Download 178de7e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T13:55 CET (sv-comp)

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

Trying to find witnesses for program (64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7, sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float1_true-unreach-call_true-termination.i, 64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/64206bd16f0fd979fec25483dda19e119f22bf0247f74a3d10d5071b9bba1db7.json

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