-
DDebugger
- Referenced in 15 articles
[sw09904]
- equational subset of rewriting logic, and rewrites and sets of reachable terms through rules ... high-performance 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 (MPI-based), and multi-core reachability (including multi-core 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 real-time logic for specifying properties of event-recording 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...
-
CLPS-B
- 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 logic-based 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...
-
D-Finder
- Referenced in 16 articles
[sw00200]
- D-Finder 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...