FloVer issueshttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues2018-08-22T10:13:04Zhttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/10Look into using Taylor polynomials for transcendental functions2018-08-22T10:13:04ZHeiko BeckerLook into using Taylor polynomials for transcendental functionsThe multivariate case seems interesting.
If we implement them it would also be interesting if we could make them parametric in the degree of approximation (i.e. `n` for an `n`-th order taylor polynomial)The multivariate case seems interesting.
If we implement them it would also be interesting if we could make them parametric in the degree of approximation (i.e. `n` for an `n`-th order taylor polynomial)https://gitlab.mpi-sws.org/AVA/FloVer/-/issues/11Implement interval validation with memorization2018-08-17T13:46:01ZHeiko BeckerImplement interval validation with memorizationImplementing `validIntervalbounds` similar to `validAffineBounds` and `getValidMap` allows to return an interval map and use accumulators to speed up computations. It further allows to implement Interval Subdivision as a range analysis.Implementing `validIntervalbounds` similar to `validAffineBounds` and `getValidMap` allows to return an interval map and use accumulators to speed up computations. It further allows to implement Interval Subdivision as a range analysis.https://gitlab.mpi-sws.org/AVA/FloVer/-/issues/1Add verbose versions of validator functions2018-07-17T11:26:05ZHeiko BeckerAdd verbose versions of validator functionsAll of the implemented validator functions current return a result of type `:bool`. For debugging failed certificates, it would be handy to have a verbose version of each validator which returns an option containing the failed expression if any or `None` otherwise.All of the implemented validator functions current return a result of type `:bool`. For debugging failed certificates, it would be handy to have a verbose version of each validator which returns an option containing the failed expression if any or `None` otherwise.https://gitlab.mpi-sws.org/AVA/FloVer/-/issues/9Port functions reasoning about options in HOL4 to monad_syntax2018-07-12T08:39:59ZHeiko BeckerPort functions reasoning about options in HOL4 to monad_syntaxhttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/2Unify input for both in-logic scripts and binaries to be custom, parsed strings2018-03-07T09:44:28ZHeiko BeckerUnify input for both in-logic scripts and binaries to be custom, parsed stringsThis will allow to develop more elaborate checkers, that could compute information if it is not present in the certificate, for example a user might only specify roundoff errors and consequently we would need to compute the ranges dynamically.This will allow to develop more elaborate checkers, that could compute information if it is not present in the certificate, for example a user might only specify roundoff errors and consequently we would need to compute the ranges dynamically.