
RealCertify
 Referenced in 7 articles
[sw28191]
 RealCertify: a Maple package for certifying nonnegativity. Let Q (resp. R) be the field ... classical algorithmic problem for symbolic computation. The Maple package extsc{RealCertify} tackles this decision problem...

RookWalks
 Referenced in 2 articles
[sw11424]
 them. For the moment, however, these computations are feasible only for low dimensions. We pose ... challenge to develop algorithms which can also certify the correctness of the equations we found...

KBCV
 Referenced in 3 articles
[sw19459]
 equations into rewrite rules; all other computations (including necessary termination checks) are performed internally. Apart ... Finally, the tool outputs proofs in a certifiable format...

sccf
 Referenced in 2 articles
[sw37297]
 mixedinteger convex programming and yields computationally tractable lower bounds. We illustrate our heuristic methods ... examples and use the perspective transformation to certify that the solutions are relatively close...

Real_Impl
 Referenced in 2 articles
[sw29247]
 also developed algorithms to precisely compute roots of a rational number, and to perform ... factors. Our results have been used to certify termination proofs which involve polynomial interpretations over...

DPCM
 Referenced in 1 article
[sw03177]
 this paper, we present and apply a computerassisted method in order to prove ... solutions. We also establish a precise and certified description of the solutions...

MMTTeX
 Referenced in 2 articles
[sw31595]
 oriented ones such as proof assistants and computer algebra systems on the other hand have ... communicating mathematical knowledge and the latter at certifying its correctness. MMTTeX aims at combining...

Ball
 Referenced in 1 article
[sw26708]
 Ball package to speed up computation to the best of our ability. Two real data ... studies have been performed and the results certify the powerfulness of Ball package in analyzing...

NeuroDiff
 Referenced in 1 article
[sw42704]
 catastrophes, there is a growing interest in certifying the equivalence of two structurally similar neural ... practice for deploying trained neural networks on computationally and energyconstrained devices, which raises...

LEMA
 Referenced in 1 article
[sw11265]
 towards a language for reliable arithmetic. Generating certified and efficient numerical codes requires information ranging ... language does not encompass the implementation on computers. Indeed various arithmetics may be involved, like ... used during the automatic generation of certified numerical codes. Such a generation process typically involves...

SNAP
 Referenced in 1 article
[sw11257]
 package for Mathematica provides various functions to compute approximate algebraic properties including approximate ... that, we can continue approximate calculations under certified tolerances without special skills in symbolicnumeric...

ROSCoq
 Referenced in 2 articles
[sw13285]
 present ROSCoq, a framework for developing certified Coq programs for robots. ROSCoq subsystems communicate using ... programs use CoRN’s exact, yet fast computations on reals, thus enabling accurate reasoning about...

Bedrock
 Referenced in 4 articles
[sw28530]
 language”: we introduce an expressive notion of certified lowlevel macros, sufficient to build ... execution of functional Coq programs that compute programs in our intermediate language...

ConCert
 Referenced in 1 article
[sw21363]
 fundamental to the establishment of a grid computing framework where all (not just large organizations ... novel solution based on the notion of certified code that upholds safety, security, and privacy...

IMP+Exc
 Referenced in 1 article
[sw28535]
 annotating terms with “decorations” that describe what computational (side) effect evaluation of a term ... this encoding is used to certify some program equivalence proofs...

Braga Method
 Referenced in 1 article
[sw42394]
 Braga method: extracting certified algorithms from complex recursive schemes in Coq. We present the Braga ... linked together: an inductive description of the computational graph of an algorithm and an inductive...

DiffRNN
 Referenced in 1 article
[sw42701]
 first differential verification method for RNNs to certify the equivalence of two structurally similar neural ... then solving constrained optimization problems to compute tight bounding boxes on nonlinear surfaces...

RandomObjects
 Referenced in 0 articles
[sw31687]
 translated into a construction function that computes φ(P) for a given P ∈ℙn ... Attempts. One is also interested in certifying the constructed object meaning that it satisfies certain...

ACETAF
 Referenced in 7 articles
[sw00014]
 ACETAF: A software package for computing validated bounds...