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).
Key | Value |
programName | sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i |
programSHA | 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a |
witnessName | results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.newton_1_2_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | 29e335ccd1a03759ef943c5ae12aaed9ea8b8a5faa513228a7aded9ee93c9ac5 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T19:09:05+01:00 |
producer | CPAchecker 1.6.1-svn 26725 |
program-sha256 | 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a |
programfile | ../../sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i |
programhash | b8ecbeb256f9e93db9e3c1caf2e70b14230dc159 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/29e335ccd1a03759ef943c5ae12aaed9ea8b8a5faa513228a7aded9ee93c9ac5.graphml |
witness-sha256 | 29e335ccd1a03759ef943c5ae12aaed9ea8b8a5faa513228a7aded9ee93c9ac5 |
witness-size | 6063 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f320ba7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T23:12 CET (comp) | ||
0880864 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:20:11+01:00 | 7c5ea82 | |
10bc748 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:17:48+01:00 | 631448b | |
a49ae04 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:02:34+01:00 | 7b5da32 | |
4afcacb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-08T00:37:11+01:00 | 2912213 | |
f6f3a16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-07T23:47:29+01:00 | 5fba0f9 | |
d16c548 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-05T19:13:17+01:00 | 74941ba | |
0ed68f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-05T19:02:53+01:00 | e9cf35e | |
51916dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-04T02:07:49+01:00 | f320ba7 | |
a3463a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-11-30T16:11:35+01:00 | 77a077d | |
77a077d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 5 | 2019-11-30T08:40:43+01:00 | ||
2912213 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 5 | 2019-12-07T13:37:54+01:00 | ||
631448b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 5 | 2019-12-01T02:54:20+01:00 | ||
5fba0f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | BRICK | 3 | 2019-12-07T22:00:06Z | ||
bd3022f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:37 CET (comp) |
Found 14 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fb0d218 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:16 CET (sv-comp) | ||
a5d5299 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 5 | 2018-12-10T17:38:07+01:00 | ||
df9d3fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 5 | 2018-12-08T02:58:11+01:00 | ||
ebad8d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T20:18:17+01:00 | a5d5299 | |
24fd5e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T07:33:31+01:00 | df9d3fb | |
b7a530f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T02:40:45+01:00 | 83e2d93 | |
ec3c1b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T16:54:15+01:00 | fb0d218 | |
e9037ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:43:20+01:00 | 6e23d88 | |
9745fa7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:12:52+01:00 | 2eaa70b | |
f89e7fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T08:43:13+01:00 | dbc4eeb | |
f816252 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T08:13:28+01:00 | 2f4c6f7 | |
932c93e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T07:50:59+01:00 | 55da62e | |
2eaa70b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-05T17:43:59+01:00 | ||
5993f96 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:02 CET (sv-comp) |
Found 18 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
29e335c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 6 | 2017-11-30T19:09:05+01:00 | ||
2bd4764 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 7 | 2017-12-01T21:19:39+01:00 | ||
934cc1e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:38 CET (sv-comp) | ||
7c34142 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T19:40:59.286150 | ||
aeb96dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T15:35:38.781281 | ||
bf5916e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T01:17:32.385528 | ||
b61834f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T13:06:16.458630 | ||
3ce12b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
84fedba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-03T04:46:05+01:00 | f38d036 | |
bf59774 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-02T08:52:23+01:00 | b6d89c3 | |
bc1163d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-02T00:34:40+01:00 | a62c320 | |
1a5a1de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T22:49:51+01:00 | 192d111 | |
0d33dd5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T07:19:41+01:00 | 6d99fd5 | |
bda4b6b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T06:15:31+01:00 | 3601d0b | |
03a8f7f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 5 | 2017-12-01T00:28 CET (sv-comp) | ||
fec266c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 10 | 2017-11-30T12:00 CET (sv-comp) | ||
73ba2da | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T14:11 CET (sv-comp) | ||
92781e1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 10 | 2017-12-01T15:13 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i, 8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8b358c669595b17c1b7679ba80e4607d853df728039ac2c239e315ef03e2c28a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |