
DDebugger
 Referenced in 15 articles
[sw09904]
 equational subset of rewriting logic, and rewrites and sets of reachable terms through rules ... highperformance system based on rewriting logic. We illustrate its use with an example...

Breach
 Referenced in 24 articles
[sw20822]
 latter is used to perform approximate reachability analysis and parameter synthesis. A major novel feature ... robust monitoring of metric interval temporal logic (MITL) formulas. The application domain of Breach ranges...

Sapo
 Referenced in 4 articles
[sw23566]
 satisfies a given specification. Sapo can represent reachable sets as unions of boxes, parallelotopes ... while specifications are formalized as Signal Temporal Logic (STL) formulas...

MLAT
 Referenced in 3 articles
[sw00582]
 logic has enough expressive power to describe properties of heaps, such as reachability. Moreover...

LTSmin
 Referenced in 21 articles
[sw07214]
 distributed reachability (MPIbased), and multicore reachability (including multicore compression and incremental hashing ... algorithms), partial order reduction and linear temporal logic...

ILLTP
 Referenced in 2 articles
[sw40829]
 compare their proofs using a linear logic based prover with focusing. In order to enhance ... reachability problems for Petri nets and encode such problems as linear logic sequents, thus enlarging...

Tempo
 Referenced in 5 articles
[sw11778]
 This algorithm is based on a forward reachability analysis and uses a symbolic representation ... Tempo. We also develop a realtime logic for specifying properties of eventrecording automata...

MARCIE
 Referenced in 8 articles
[sw12882]
 MARCIE  model checking and reachability analysis done efficiently. MARCIE is a tool for the analysis ... properties to model checking of established temporal logics. MARCIE’s analysis engines for bounded Petri...

CLPSB
 Referenced in 7 articles
[sw00132]
 evaluation of B formal specifications using Constraint Logic Programming with sets. This approach is used ... reduces the number of states in a reachability graph. We illustrate this approach by comparing...

Pyhybridanalysis
 Referenced in 3 articles
[sw14549]
 framework developed in [CPP08] to reduce the reachability problem over hybrid automata to the satiability ... formula in the opportune theory. Automata are logicbased and their are defined as described...

ConfigChecker
 Referenced in 1 article
[sw28842]
 diagrams (BDDs). We then use computation tree logic (CTL) and symbolic model checking to investigate ... packet in the network and verify network reachability and security requirements. Thus, our contributions...

HAGAR
 Referenced in 1 article
[sw02336]
 graph processors. Graph algorithms, such as vertex reachability, transitive closure, and shortest path, are fundamental ... reconfigurable hardware that, along with support logic and software in a microprocessor, accelerates a core ... HAGAR). We describe HAGAR implementations for graph reachability and shortest path. Reachability is a building...

ACL2
 Referenced in 283 articles
[sw00060]
 ACL2 is both a programming language in which...

CoCoA
 Referenced in 654 articles
[sw00143]
 CoCoA is a system for Computations in Commutative...

Coq
 Referenced in 1880 articles
[sw00161]
 Coq is a formal proof management system. It...

CUTE
 Referenced in 65 articles
[sw00177]
 CUTE: a concolic unit testing engine for C...

DFinder
 Referenced in 16 articles
[sw00200]
 DFinder tool implements a compositional method for...

IMITATOR
 Referenced in 29 articles
[sw00439]
 IMITATOR is a software tool for parametric verification...

Isabelle
 Referenced in 698 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

Maple
 Referenced in 5363 articles
[sw00545]
 The result of over 30 years of cutting...