• 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 non-linear 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 as­ser­tions. Furthermore, it can check ANSI-C 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 P-solvable loops. Aligator contains routines for checking the P-solvability 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 loop-checking algorithm using a cache of satisfiable worlds created...
  • CakeML

  • Referenced in 49 articles [sw08799]
  • implemented as an interactive read-eval-print loop (REPL) in x86-64 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 four-loop level is highly complicated and the equations ... with computer-assisted derivations. We have checked correctness of the program by recomputing already-known...
  • 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 ... gradient-based 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 one-loop level for a wide variety ... show the validity of the gauge check. These cover fermion-fermion 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]
  • colour-ordered n-gluon amplitudes at one-loop order in pure Yang--Mills 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 interpolation-based function summaries ... tool incorporates a counter-example-guided 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. Multi-criticality real-time systems require protected-mode ... 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, less-trusted components. ARMor guarantees ... rewriting a binary to put a check in front of every potentially dangerous operation...