• CBMC

  • Referenced in 86 articles [sw09719]
  • CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also ... supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety...
  • INTLAB

  • Referenced in 472 articles [sw04004]
  • slopes (sequential approach, slow for many variables) verified integration of (simple) univariate functions univariate ... slow) multiple precision interval arithmetic with error bounds (does the job, slow...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • UCLID: As a verifier, for term-level bounded model checking, correspondence checking, deductive verification ... verification, analyzing software for security exploits, and verifying distributed algorithms...
  • ACETAF

  • Referenced in 7 articles [sw00014]
  • ACETAF: A software package for computing validated bounds for Taylor coefficients of analytic functions. This ... presents methods for practical computation of verified bounds for Taylor coefficients of analytic functions. These...
  • C2e2

  • Referenced in 11 articles [sw20139]
  • Engine (C2E2) is a tool for verifying bounded-time invariant properties of hybrid system...
  • PHAVer

  • Referenced in 118 articles [sw04123]
  • ground as a potentially powerful tool for verifying hybrid systems – yet it has remained severely ... properties of hybrid systems with piecewise constant bounds on the derivatives. Affine dynamics are handled...
  • MRMC

  • Referenced in 73 articles [sw04129]
  • Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL ... support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise...
  • VSDP

  • Referenced in 12 articles [sw04003]
  • that is designed for the computation of verified results in conic programming. The current version ... computing rigorous error bounds of the true optimal value, verified enclosures of ε-optimal solutions...
  • AFiD_GPU

  • Referenced in 7 articles [sw24939]
  • unprecedented in thermally-driven wall-bounded turbulence. To verify the accuracy of the code, turbulent...
  • SMACK

  • Referenced in 9 articles [sw23311]
  • default mode, assertions are verified up to a given bound on loop iterations and recursion...
  • ESBMC

  • Referenced in 8 articles [sw09946]
  • ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo ... allows the verification engineer (i) to verify single- and multi-threaded software (with shared variables ... array bounds, atomicity and order violations, deadlock and data race; (iii) to verify programs that...
  • core 2

  • Referenced in 7 articles [sw04960]
  • based on iterative verified approximations, combined with constructive zero bounds. This paper describes Core...
  • MAVEN

  • Referenced in 10 articles [sw07659]
  • aspect is bound (woven) to an underlying system. The MAVEN tool verifies the correctness...
  • Crust

  • Referenced in 1 article [sw34343]
  • Crust: A Bounded Verifier for Rust (N). Rust is a modern systems language that provides ... tool combining exhaustive test generation and bounded model checking to detect memory safety errors...
  • DiVer

  • Referenced in 10 articles [sw01938]
  • verifying large designs. The engines with their respective roles are as follows: Bounded Model Checking ... combination with PBIA in BMC for verifying embedded memory systems with multiple memories (with multiple...
  • Hybrid Trace Verifier

  • Referenced in 2 articles [sw20335]
  • Computing bounded reach sets from sampled simulation traces. This paper presents an algorithm which uses ... algorithm in a tool, Hybrid Trace Verifier (HTV), uses Mathwork’s Simulink/Stateflow (SLSF) environment ... overapproximation relies on computing error bounds in the dynamics obtained from the formal model. Verification...
  • CPBPV

  • Referenced in 5 articles [sw00164]
  • programming framework for bounded program verification. This paper studies how to verify the conformity ... proposes a novel constraint-programming framework for bounded program verification (CPBPV). The CPBPV framework uses...
  • ACRITH-XSC

  • Referenced in 49 articles [sw00015]
  • deliver results of high accuracy which are verified to be correct by the computer. Thus ... complete sample program for computing continuous bounds on the solution of an initial value problem...
  • Edmonds-Karp

  • Referenced in 6 articles [sw28548]
  • formally prove a bound on its complexity. Further refinement yields a verified implementation, whose execution...
  • TESTAS

  • Referenced in 19 articles [sw00957]
  • strictly locally testable, or piecewise testable. The bounds on order of local testability of transition ... testability of transition graph is verified. Some new effective polynomial time algorithms are used. These...