• PAT

  • Referenced in 38 articles [sw13258]
  • simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with ... partial order reduction, symmetry reduction, process counter abstraction, parallel model checking...
  • Eden

  • Referenced in 28 articles [sw22186]
  • this code interacts with the distributed RunTime System (RTS) for Eden. This translation is done ... translated into PEARL (Parallel Eden Abstract Reduction Language), the parallel functional language of DREAM...
  • ELAN

  • Referenced in 108 articles [sw02179]
  • environment for specifying and prototyping deduction systems in a language based on rules controlled ... takes from functional programming the concept of abstract data types and the function evaluation principle ... existing rewriting-based languages where the term reduction strategy is hard-wired and not accessible ... both the logical framework in which deduction systems can be expressed and combined...
  • ABS

  • Referenced in 31 articles [sw21211]
  • abstract behavioral specification language for designing executable models of distributed object-oriented systems. The language ... issues for ABS and formalize the type system and semantics of Core ABS, a calculus ... Core ABS, we prove a subject reduction property which shows that well-typedness is preserved...
  • fc2tools

  • Referenced in 11 articles [sw12386]
  • model-based, automatic verification of distributed communicating systems. It is developed jointly by INRIA ... syntax and semantics; verification by compositional reductions and abstraction; alternative or combined use of explicit...
  • BFComp

  • Referenced in 3 articles [sw18654]
  • approximately equivalent abstraction, thereby enabling approximate model-order reduction of dynamical systems...
  • DiVer

  • Referenced in 10 articles [sw01938]
  • model checking platform for verifying large scale systems. We present a SAT-based model checking ... falsification, Proof-based Iterative Abstraction (PBIA) for model reduction, SAT-based Unbounded Model Checking ... PBIA in BMC for verifying embedded memory systems with multiple memories (with multiple ports...
  • Rapture

  • Referenced in 7 articles [sw13409]
  • probabilistic transition system). The originality of the tool is to provide two reduction techniques that ... limit the state space explosion problem : automatic abstraction and refinement algorithms, and a so-called...
  • FODD-Planner

  • Referenced in 15 articles [sw07747]
  • make the approach practical. These include new reduction operators that decrease the size ... planning system, FODD-Planner, for solving relational stochastic planning problems. The system is evaluated ... shows competitive performance with top ranking systems. This is the first demonstration of feasibility ... this approach and it shows that abstraction through compact representation is a promising approach...
  • Rebeca

  • Referenced in 9 articles [sw09422]
  • formal foundation for modeling concurrent and distributed systems which is designed in an effort ... introduce compositional verification, abstraction, symmetry and partial order reduction techniques for reducing the state space...
  • CARIBOO

  • Referenced in 14 articles [sw10064]
  • languages, where a program is a rewrite system and query evaluation consists in rewriting ... Computing AbstRaction for Induction Based termination prOOfs), allows proving termination under specific reduction strategies, which...
  • Boom

  • Referenced in 2 articles [sw01318]
  • Boom implements a recent variant of counter abstraction, where thread counters are used ... Karp-Miller tree construction for vector addition systems, resulting in a reachability engine for programs ... reduction methods. Boom is intended for model checking system-level code via predicate abstraction...
  • Alfalfa

  • Referenced in 3 articles [sw09414]
  • heterogeneous abstract machine model consisting of both graph reduction and stack oriented execution. Alfalfa consists ... components, a compiler and a run-time system. The source language, Alfl, contains no constructs...
  • PECANS

  • Referenced in 6 articles [sw02161]
  • approach for the modeling of complex physical systems and a parallel programming environment that implements ... methodological approach is based on a reduction process of a physical phenomenon in components; each ... components are represented by the CA network abstraction. A CA is a bidimensional grid...
  • CRSX

  • Referenced in 4 articles [sw23630]
  • pure Combinatory Reduction Systems with full strong reduction (but no specified reduction strategy). - Rule ... ease parsing directly into higher-order abstract syntax (as well as permitting ... rules files). - Experimental (and evolving) sort system to help rule management. - Compiler from (well-sorted...
  • TRAM

  • Referenced in 2 articles [sw03369]
  • TRAM is an abstract machine for order-sorted conditional term rewritting systems (OSCTRSs). The OSCTRSs ... TRAM adopts the E-strategy as its reduction strategy. Parallel TRAM is a parallel variant...
  • pFaces

  • Referenced in 3 articles [sw30630]
  • digital controllers are algorithmically synthesized for concrete systems, satisfying complex high-level requirements. Unfortunately ... capabilities, novel parallel algorithms are designed for abstraction-based controller synthesis. Then, they are implemented ... Hardware Accelerators (HWAs). Results show remarkable reduction in the computation time by several orders...
  • modred

  • Referenced in 4 articles [sw17490]
  • library for model reduction, modal analysis, and system identification of large systems and datasets ... larger and more complicated datasets, preserves the abstraction of vectors as elements of a vector...
  • Merlin

  • Referenced in 5 articles [sw23076]
  • characterize this approximation as a probabilistic abstraction, using the theory of probabilistic refinement developed ... McIver and Morgan. We solve the resulting system of probabilistic constraints using factor graphs, which ... positives being removed; this constitutes a 15% reduction in the CAT.NET false positive rate...
  • VEST

  • Referenced in 2 articles [sw16763]
  • VEST (Vector Einstein Summation Tools), that performs abstract vector calculus computations in Mathematica. Through ... vector identities that are not recognized by reduction, subsequently applying these to simplify large expressions ... Lagrangians for the single particle guiding center system in plasma physics, a computation which illustrates...