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

SIFT
 Referenced in 504 articles
[sw16554]
 known objects using a fast nearestneighbor algorithm, followed by a Hough transform to identify ... single object, and finally performing verification through leastsquares solution for consistent pose parameters. This...

HyTech
 Referenced in 308 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...

SpaceEx
 Referenced in 51 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...

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

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 computeraided verification scripting environment ... Integrated Developer Environment for algorithmic verification applications. Jtlv may be viewed...

nuXmv
 Referenced in 9 articles
[sw18526]
 nuXmv with stateoftheart verification algorithms. For infinitestate systems, it extends ... been used in several industrial projects as verification backend, and it is the basis...

NuSMV
 Referenced in 276 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 semialgebraic ... 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 MOdelCHecking 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...