Results 1 to 20 of 202
Sort by:

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