
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 rewardbounded 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 highperformance 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 machinelearning 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 ... computerassisted 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 SATsolvers. 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 nonlinear 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...