• C-XSC

  • Referenced in 106 articles [sw00181]
  • programming environment for verified scientific computing and numerical data processing. C-XSC is a tool ... numerical algorithms delivering highly accurate and automatically verified results. It provides a large number ... package is available for all computers with a C++ compiler translating the AT&T language...
  • Pinocchio

  • Referenced in 28 articles [sw10193]
  • Pinocchio: Nearly practical verifiable computation. To instill greater confidence in computations outsourced to the cloud ... Pinocchio, a built system for efficiently verifying general computations while relying only on cryptographic assumptions ... only 288 bytes, regardless of the computation performed or the size of the inputs ... into programs that implement the verifiable computation protocol...
  • INTLAB

  • Referenced in 406 articles [sw04004]
  • very fast) automatic differentiation (forward mode, vectorized computations, fast) Gradients (to solve systems of nonlinear ... slopes (sequential approach, slow for many variables) verified integration of (simple) univariate functions univariate...
  • HyTech

  • Referenced in 320 articles [sw04125]
  • analysis of embedded systems. HyTech computes the condition under which a linear hybrid system satisfies ... continuous components, and temporal requirements are verified by symbolic model checking. If the verification fails...
  • Ellipsoidal Toolbox

  • Referenced in 34 articles [sw10826]
  • systems with disturbances. It can be verified if computed reach sets intersect with given ellipsoids...
  • VERSOFT

  • Referenced in 21 articles [sw10881]
  • collection of verification files for computing verified solutions of various numerical linear algebraic problems having...
  • ParLinSys

  • Referenced in 19 articles [sw06461]
  • supplements the library C++-Toolbox. ParLinSys computes verified enclosure of the solution set of parametric...
  • ACRITH-XSC

  • Referenced in 49 articles [sw00015]
  • high accuracy which are verified to be correct by the computer. Thus there...
  • Cosy

  • Referenced in 87 articles [sw07711]
  • various advanced concepts of modern scientific computing. COSY currently has more than 2000 registered users ... been extensively cross-checked and verified. The COSY system consists of the following parts...
  • intpakX

  • Referenced in 11 articles [sw00445]
  • complex disc arithmetic. As applications, verified computation of zeroes (Interval Newton Method) with the possibility...
  • Geppetto

  • Referenced in 7 articles [sw31791]
  • Geppetto: Versatile Verifiable Computation. Cloud computing sparked interest in Verifiable Computation protocols, which allow ... computations to remote parties. Recent work has dramatically reduced the client’s cost to verify ... reduces the cost of sharing state between computations (e.g, For MapReduce) or within a single ... computation by up to two orders of magnitude. Via a careful choice of cryptographic primitives...
  • INTERVAL_ARITHMETIC

  • Referenced in 10 articles [sw04681]
  • Interval arithmetic is useful in automatically verified computations, that is, in computations in which...
  • VSDP

  • Referenced in 12 articles [sw04003]
  • package that is designed for the computation of verified results in conic programming. The current ... functions for computing rigorous error bounds of the true optimal value, verified enclosures...
  • Cadabra

  • Referenced in 77 articles [sw00097]
  • lends itself well to the routine computations required in general relativity. Here, we present ... showing how Cadabra may be used, including verifying that the Levi-Civita connection...
  • zk-SNARK

  • Referenced in 11 articles [sw22495]
  • when communication is expensive, or the verifier is computationally weak. Existing zk-SNARK implementations have ... down” all intermediate values of the entire computation, and then conducting global operations such ... acceptance of the proof system’s own verifier (and correctness of the program’s latest ... been realized in practice, due to enormous computational cost. Using new elliptic-curve cryptographic techniques...
  • Metamath

  • Referenced in 15 articles [sw13309]
  • proofs that can be verified by a computer program...
  • kv

  • Referenced in 5 articles [sw31712]
  • Library for Verified Numerical Computation. A set of libraries for verified numerical computations (kv library ... this page. For overview of verified numerical computation and kv library, please see the slide...
  • Cadence SMV

  • Referenced in 27 articles [sw07795]
  • formally verify temporal logic properties of finite state systems, such as computer hardware designs. That ... vectors or a simulation test bench, you verify your design for all possible input sequences...
  • UNITY

  • Referenced in 173 articles [sw13461]
  • analysis in UNITY. We evaluate UNITY -- a computational model, specification language and proof system defined ... methodology provides a means to independently verify the correctness of the transition systems...
  • MRMC

  • Referenced in 66 articles [sw04129]
  • Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL ... features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property...