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/newton_2_4_true-unreach-call_true-termination.i
programSHA 27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.newton_2_4_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 55371cee459235a2ff736a61a036cde7d5dd8ee33ddc1434394976db72d96296

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/55371cee459235a2ff736a61a036cde7d5dd8ee33ddc1434394976db72d96296.json

Key Value
architecture 32bit
creationtime 2018-12-07T19:27:25.614306
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i
programhash c6ebcad508768cfd23c1e789e2415fe511a2a196
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/55371cee459235a2ff736a61a036cde7d5dd8ee33ddc1434394976db72d96296.graphml
witness-sha256 55371cee459235a2ff736a61a036cde7d5dd8ee33ddc1434394976db72d96296
witness-size 3414
witness-type correctness_witness

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

Trying to find witnesses for program (27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46, sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i).

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

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

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

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

Found 13 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i, 27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a182fcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:30 CET (comp)
Download d62aa3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:26:59+01:00 Download a40a259
Download 06760dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:03:00+01:00 Download 7b58e61
Download f7d5e49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:36:18+01:00 Download 8f61803
Download becf9be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:47:31+01:00 Download 4ad3cde
Download 0350464 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:12:51+01:00 Download d387bf8
Download 987e296 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:02:53+01:00 Download 0a2bb71
Download 14fb843 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:08:00+01:00 Download a182fcb
Download dc1e661 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T17:25:04+01:00 Download d05c2d3
Download d05c2d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T10:13:54+01:00
Download 8f61803 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 6 2019-12-07T20:35:51+01:00
Download 4ad3cde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:38:45Z
Download be24d1d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:33 CET (comp)

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

Trying to find witnesses for program (27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46, sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i).

Found 14 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i, 27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f3c6e0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T15:34 CET (sv-comp)
Download fef5a5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 6 2018-12-10T18:32:08+01:00
Download d218b0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T22:56:00+01:00
Download 66f6d54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:04:04+01:00 Download fef5a5f
Download f7495da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T06:18:01+01:00 Download d218b0a
Download 26ca034 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:45:22+01:00 Download 55371ce
Download 96c688c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:53:21+01:00 Download f3c6e0b
Download f3a0faa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:43:34+01:00 Download fa9c148
Download 0a39a56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:11:54+01:00 Download 6a82dd6
Download 59e5940 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:26:58+01:00 Download 5910583
Download e178257 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:58:43+01:00 Download 2fee2c6
Download 1b22c25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:26:40+01:00 Download d52c814
Download 6a82dd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T22:13:33+01:00
Download bd271da Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:34 CET (sv-comp)

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

Trying to find witnesses for program (27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46, sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i).

Found 14 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i, 27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 611afab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T11:47:41+01:00
Download b184cad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 8 2017-12-01T22:37:09+01:00
Download 6c8bbb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:29:15.397318
Download 4957157 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:31:41.113639
Download 10575fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:49:07.422186
Download 861d93d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T18:31:17.478105
Download ab726c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T07:59:47+01:00 cbf6364
Download fa20f2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:44:47+01:00 a0db80b
Download dd1efd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:11:30+01:00 1995781
Download b141ecb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:09:00+01:00 3ffbbb2
Download 57e51d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 6 2017-11-30T13:43 CET (sv-comp)
Download 920e3cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 15 2017-12-01T03:12 CET (sv-comp)
Download c38d335 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T14:15 CET (sv-comp)
Download e853a2c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T15:06 CET (sv-comp)

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

Trying to find witnesses for program (27aa3319a96e3f5b0c3b20666a96e665feb85bd034074efc69dca0f28eeeda46, sv-benchmarks/c/floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i).

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

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