• MOCHA

  • Referenced in 83 articles [sw12935]
  • vehicle for development of new verification algorithms and approaches. MOCHA is available in two versions...
  • SIFT

  • Referenced in 500 articles [sw16554]
  • known objects using a fast nearest-neighbor algorithm, followed by a Hough transform to identify ... single object, and finally performing verification through least-squares solution for consistent pose parameters. This...
  • HyTech

  • Referenced in 305 articles [sw04125]
  • verified by symbolic model checking. If the verification fails, then HyTech generates a diagnostic error ... trace. The standard reference to the HyTech algorithm is [1], and the standard reference...
  • UnitWalk

  • Referenced in 34 articles [sw00993]
  • from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms...
  • UFO

  • Referenced in 16 articles [sw09570]
  • researchers designing and experimenting with verification algorithms. It allows definition of different abstract post operators...
  • SpaceEx

  • Referenced in 47 articles [sw10939]
  • SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems ... algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid...
  • LTSmin

  • Referenced in 13 articles [sw07214]
  • checking (e.g., for state space generation and verification of safety properties), reachability with symbolic state ... language modules, PINS optimizations, and model checking algorithms ... other hand, the implementation of a verification algorithm based on the PINS matrix automatically...
  • InVeSt

  • Referenced in 10 articles [sw12034]
  • InVeSt: a tool for the verification of invariants. A very important class of properties ... algorithmic methods. In this paper we present the tool In VeSt which supports the verification ... systems. In VeSt integrates deductive and algorithmic verification principles for the verification of invariance properties...
  • CESAR

  • Referenced in 139 articles [sw08510]
  • Specification and verification of concurrent systems in CESAR. The aim of this paper ... CESAR allows the progressive validation of the algorithmic description of a system of communicating sequential ... given set of specifications. The algorithmic description is done in a high level language inspired ... fixed points of monotonic predicate transformers. The verification of a system consists in obtaining...
  • JTLV

  • Referenced in 7 articles [sw08859]
  • Jtlv: A Framework for Developing Verification Algorithms. Jtlv is a computer-aided verification scripting environment ... Integrated Developer Environment for algorithmic verification applications. Jtlv may be viewed...
  • nuXmv

  • Referenced in 9 articles [sw18526]
  • nuXmv with state-of-the-art verification algorithms. For infinite-state systems, it extends ... been used in several industrial projects as verification back-end, and it is the basis...
  • NuSMV

  • Referenced in 274 articles [sw04131]
  • verification tools, as a testbed for formal verification techniques, and applied to other research areas ... package use in the Bounded Model Checking algorithms...
  • DISCOVERER

  • Referenced in 35 articles [sw07719]
  • advances in program verification indicate that various verification problems can be reduced to semi-algebraic ... consists of polynomial equations and polynomial inequalities. Algorithms for quantifier elimination of real closed fields ... problems. To overcome the bottleneck of program verification with a symbolic approach ... invented new theories and algorithms [32,30,35] for SAS solving and partly implemented them...
  • YOGI

  • Referenced in 12 articles [sw13094]
  • testing. Yogi implements the Dash algorithm which performs verification by combining directed testing and abstraction ... properties. We find that the new algorithm enables Yogi to scale much better than Slam...
  • ODESSA

  • Referenced in 28 articles [sw00647]
  • Algorithm 658_ ODESSA - An ordinary differential equation solver with explicit simultaneous sensitivity analysis. ODESSA ... program usage and optional capabilities, installation, and verification considerations are addressed herein...
  • FLASH

  • Referenced in 45 articles [sw02233]
  • computations. We called FLASH our algorithm and we also proposed SFLASH, a version that ... smaller public key and faster verification though one should be even more careful about...
  • Spacer

  • Referenced in 7 articles [sw19496]
  • based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular...
  • SPHIN

  • Referenced in 4 articles [sw19754]
  • syntax of PROMELA and the verification algorithms based on the expected semantics. We demonstrate...
  • UCLID

  • Referenced in 22 articles [sw04657]
  • microprocessor design verification, analyzing software for security exploits, and verifying distributed algorithms...
  • jMocha

  • Referenced in 2 articles [sw24777]
  • model checker jMocha (Java MOdel-CHecking Algorithm) is based on this theme. Instead of manipulating ... interactive software environment for specification, simulation and verification, and is intended ... vehicle for the development of new verification algorithms and approaches. It is written in Java ... rapid and structured development of new verification algorithms. jMocha is available publicly...