
MetTeL
 Referenced in 15 articles
[sw11990]
 generalisation of a standard loop checking mechanism or unrestricted blocking...

GenSSI
 Referenced in 11 articles
[sw10712]
 building is often regarded as an iterative loop involving several tasks, among which the estimation ... identifiability of any tentative model should be checked ... beginning of the model building loop. However, checking this property for arbitrary nonlinear dynamic...

SatAbs
 Referenced in 39 articles
[sw12804]
 model checking tool, SatAbs, that implements a predicate abstraction refinement loop. Existing software verification tools...

CBMC
 Referenced in 78 articles
[sw09719]
 specified assertions. Furthermore, it can check ANSIC and C++ for consistency with ... verification is performed by unwinding the loops in the program and passing...

Aligator
 Referenced in 10 articles
[sw00029]
 class of Psolvable loops. Aligator contains routines for checking the Psolvability of loops ... solving recurrences and deriving closed forms of loop variables, computing the ideal of polynomial invariants ... variable elimination, invariant filtering and completeness check of the resulting set of invariants...

MODPROF
 Referenced in 2 articles
[sw21543]
 syntactic branching, and an enhanced loopchecking algorithm using a cache of satisfiable worlds created...

CakeML
 Referenced in 49 articles
[sw08799]
 implemented as an interactive readevalprint loop (REPL) in x8664 machine code ... breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary...

Lotrecscheme
 Referenced in 3 articles
[sw10967]
 merge two worlds when the system check a loop (for instance for S4): merging instead...

Forcer
 Referenced in 18 articles
[sw28330]
 Since the program structure at the fourloop level is highly complicated and the equations ... with computerassisted derivations. We have checked correctness of the program by recomputing alreadyknown...

NMSSMTools
 Referenced in 26 articles
[sw04069]
 Higgs spectrum includes leading electroweak corrections, two loop terms and propagator corrections. The computation ... decays. Each point in parameter space is checked against negative Higgs boson searches...

Autograd
 Referenced in 21 articles
[sw22077]
 large subset of Python’s features, including loops, ifs, recursion and closures ... gradientbased optimization. For more information, check out the tutorial and the examples directory...

STLlint
 Referenced in 3 articles
[sw33541]
 algorithms. Major challenges include checking the use of generic algorithms, loop analysis for interfaces...

GRACE
 Referenced in 3 articles
[sw11987]
 loop diagrams in the electroweak theory with gauge parameter independence checks. We describe the main ... Dirac and tensor algebra, implementation of the loop integrals, the generation of the matrix elements ... which have been performed at the oneloop level for a wide variety ... show the validity of the gauge check. These cover fermionfermion scattering, gauge boson scattering...

TVOC
 Referenced in 19 articles
[sw02521]
 that uses the translation validation approach to check the validity of compiler optimizations ... verification process: the first phase verifies loop transformations using the proof rule permute; the second...

NGluon
 Referenced in 17 articles
[sw06832]
 colourordered ngluon amplitudes at oneloop order in pure YangMills theory ... program may also prove useful in cross checking results obtained by other methods. In addition...

ENuSMV
 Referenced in 1 article
[sw13327]
 Bounded model checking of ETL cooperating with finite and looping automata connectives. As a complementary ... been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is rather ... temporal logic involves both finite and looping automata as connectives, all regular properties...

FunFrog
 Referenced in 6 articles
[sw06571]
 function summarization approach for software bounded model checking. It uses interpolationbased function summaries ... tool incorporates a counterexampleguided refinement loop. Experimental evaluation demonstrates competitiveness of FunFrog with...

SMACK
 Referenced in 8 articles
[sw23311]
 verified up to a given bound on loop iterations and recursion depth; it contains experimental ... implementation of algorithms for verification, model checking, and abstract interpretation...

Sequoll
 Referenced in 0 articles
[sw22322]
 Sequoll: a framework for model checking binaries. Multicriticality realtime systems require protectedmode ... such systems requires trustworthy information about loop bounds and infeasible paths. We propose sequoll ... framework for employing model checking of binary code to determine loop counts and infeasible paths...

ARMor
 Referenced in 3 articles
[sw18275]
 such as the RTOS and critical control loops from other, lesstrusted components. ARMor guarantees ... rewriting a binary to put a check in front of every potentially dangerous operation...