• RealCertify

  • Referenced in 7 articles [sw28191]
  • RealCertify: a Maple package for certifying non-negativity. 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]
  • mixed-integer 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 computer-assisted 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 energy-constrained 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 symbolic-numeric...
  • 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 low-level 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 non-linear 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...