• KeYmaeraD

  • Referenced in 0 articles [sw20142]
  • Hybrid Systems. Distributed hybrid systems present extraordinarily challenging problems for verification ... problem of automated theorem proving for distributed hybrid systems. We have designed a powerful strategy ... high computational complexity of distributed hybrid systems verification, KeYmaeraD uses a distributed proving backend...
  • SPHIN

  • Referenced in 5 articles [sw19754]
  • SPHIN, a model checker for reconfigurable hybrid systems based on the model checker SPIN ... extend the syntax of PROMELA and the verification algorithms based on the expected semantics ... modeling and verifying a reconfigurable hybrid system...
  • StocHy

  • Referenced in 5 articles [sw36937]
  • StocHy: automated verification and synthesis of stochastic processes. StocHy is a software tool ... quantitative analysis of discrete-time stochastic hybrid systems (SHS). StocHy accepts a high-level description ... Abstractions are then employed for (ii) formal verification or (iii) control (policy, strategy) synthesis. StocHy...
  • Acumen

  • Referenced in 1 article [sw36603]
  • Physical Systems requires methods and tools to support simulation and verification of hybrid (both continuous ... deliver to developers of Cyber-Physical Systems. Like verification tools, a design goal for Acumen...
  • HyComp

  • Referenced in 4 articles [sw20163]
  • HyComp takes as input networks of hybrid automata specified using the HyDI symbolic language. HyComp ... infinite-state transition system, which can be analyzed using SMT-based verification techniques...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • language, HYDI, for modeling Hybrid systems with Discrete Interaction. The purpose of the language ... model checkers for infinite-state systems to the verification of complex embedded systems design. HYDI...
  • Hybrid Trace Verifier

  • Referenced in 2 articles [sw20335]
  • deterministic hybrid systems. The implementation of the algorithm in a tool, Hybrid Trace Verifier ... dynamics obtained from the formal model. Verification results from three case studies, namely, a version ... navigation benchmark, an engine control system, and a satellite system suggest that this combined formal...
  • REDLIB

  • Referenced in 5 articles [sw21175]
  • Formal Verification of Embedded Systems. To promote the technology of dense-time system model-checking ... fixpoint calculation, parametric safety analysis of linear hybrid systems, speed-up techniques for greatest fixpoint...
  • DyverseRBT

  • Referenced in 1 article [sw41812]
  • mechanical systems with multiple contacts as an extended version of the classical hybrid automaton, which ... call MRB hybrid automaton. One of the chief characteristics of the MRB hybrid automaton ... automated verification of dynamical properties of realistic mechanical systems. We show this by the falsification...
  • EFSMT

  • Referenced in 2 articles [sw19487]
  • EFSMT by reducing a number of pivotal verification and synthesis problems to EFSMT. Exemplary problems ... control systems, distributed priority synthesis for orchestrating system components, and synthesis for hybrid control systems...
  • SAHA-Tool

  • Referenced in 1 article [sw10315]
  • powerful formalism for the representation of systems evolving according to both discrete and continuous laws ... tries to automatically verify hybrid automata properties. An important verification problem is the reachability...
  • SL2SX

  • Referenced in 1 article [sw20160]
  • scales well and can be applied to systems with highly complex dynamics ... verification techniques to Simulink models could help to overcome this limitation. Set-based verification tools ... such as SpaceEx use as underlying formalism hybrid automata, which are semantically and structurally different...
  • Aligator

  • Referenced in 10 articles [sw00029]
  • We describe the new software package Aligator for...
  • ANSYS

  • Referenced in 713 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • AXIOM

  • Referenced in 173 articles [sw00063]
  • Axiom is a general purpose Computer Algebra system...
  • BARON

  • Referenced in 361 articles [sw00066]
  • BARON is a computational system for solving nonconvex...
  • cdd

  • Referenced in 119 articles [sw00114]
  • The program cdd+ (cdd, respectively) is a C...
  • CGAL

  • Referenced in 402 articles [sw00118]
  • The goal of the CGAL Open Source Project...
  • CoCoA

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