
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 21 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 3 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...

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...

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

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 279 articles
[sw00060]
 ACL2 is both a programming language in which...

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

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

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

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

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

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

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

Mathematica
 Referenced in 6041 articles
[sw00554]
 Almost any workflow involves computing results, and that...