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

  • Referenced in 18 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...
  • 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 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...
  • D-Finder

  • Referenced in 15 articles [sw00200]
  • D-Finder 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...