• UNITY

  • Referenced in 185 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 73 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...
  • CoqEAL

  • Referenced in 5 articles [sw03703]
  • algebra, by which we mean formally verified computer algebra algorithms that can be run inside...
  • ACETAF

  • Referenced in 7 articles [sw00014]
  • This article presents methods for practical computation of verified bounds for Taylor coefficients of analytic...
  • Lurupa

  • Referenced in 4 articles [sw09980]
  • value of a linear program and compute verified enclosures of near optimal feasible points ... linear programming solver is needed to compute approximate solutions. Currently only lp_solve is supported...
  • PHoM

  • Referenced in 30 articles [sw04645]
  • compute all isolated solutions of $f(x)= 0$. The third module Verify checks whether...
  • PHAVer

  • Referenced in 118 articles [sw04123]
  • ground as a potentially powerful tool for verifying hybrid systems – yet it has remained severely ... manage the complexity of the polyhedral computations, we propose methods to conservatively limit the number...
  • Algorithm 679

  • Referenced in 65 articles [sw12583]
  • portable, implementations of algorithms on high-performance computers. The model implementation provides a portable ... required. The test software aims to verify that specialized implementations meet the specification of Level...
  • ML4PG

  • Referenced in 9 articles [sw07140]
  • ML4PG in computer algebra verification ML4PG is a machine-learning extension that provides statistical proof ... library that was devised to verify the correctness of computer algebra algorithms. In particular...
  • QuickLex

  • Referenced in 3 articles [sw23063]
  • consistent global states enumeration of distributed computations. Verifying the correctness of executions of concurrent ... state of the given concurrent or distributed computation. The method is predictive because it generates...
  • Cmodels

  • Referenced in 72 articles [sw04435]
  • Cmodels is a system that computes answer sets for either disjunctive logic programs or logic ... solver zChaff is also used for verifying the minimality of found models. The system Cmodels ... loop formulas might be large, therefore computing all of them may become computationally expensive. This...
  • DEMOCRITUS

  • Referenced in 7 articles [sw18290]
  • present work, the computational method is verified against known results. Finally, the simulation method...
  • RIM_DOM.F90

  • Referenced in 37 articles [sw25510]
  • conventional method), but also make computational results for singular domain integrals more accurate since ... been regularized. Some examples are provided to verify the correctness of the presented formulations...
  • Octave Interval

  • Referenced in 2 articles [sw13236]
  • their domain. All results are verified, because interval computations automatically keep track of any errors ... computer-assisted proofs, constraint programming, and verified computing. The implementation is based on interval boundaries...
  • Albert

  • Referenced in 19 articles [sw15065]
  • independently verified - either with a traditional mathematical proof or with an independent computation. Computer algebra...
  • EPGY

  • Referenced in 4 articles [sw28722]
  • combination of automated reasoning and symbolic computation to verify individual proof steps. The proof environment...
  • F@BOOL@

  • Referenced in 3 articles [sw21004]
  • based on SAT-solvers. A verifying compiler is computer system program that translates programs written ... language to equivalent executable programs and proves (verifies) mathematical statements specified by a human concerning ... user friendly, compact, and portable verifying compiler of annotated computational programs that uses efficient...
  • constant_estimation

  • Referenced in 2 articles [sw29872]
  • finite element method along with verified computation is proposed. In addition, the quantitative analysis...
  • core 2

  • Referenced in 7 articles [sw04960]
  • approach to algebraic number computation is based on iterative verified approximations, combined with constructive zero ... designed for applications such as non-linear computational geometry. The adaptive complexity of ENC combined...
  • Hybrid Trace Verifier

  • Referenced in 2 articles [sw20335]
  • uses simulation traces and formal models for computing overapproximations of reach sets of deterministic hybrid ... algorithm in a tool, Hybrid Trace Verifier (HTV), uses Mathwork’s Simulink/Stateflow (SLSF) environment ... simulation traces and for obtaining formal models. Computation of the overapproximation relies on computing error...