• SpaceEx

  • Referenced in 63 articles [sw10939]
  • SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems ... part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results...
  • d/dt

  • Referenced in 35 articles [sw10314]
  • inclusions. The d/dt tool for verification of hybrid systems. We describe the tool d/dt which ... provides automatic safety verification of hybrid systems with linear continuous dynamics with uncertain input...
  • KeYmaera

  • Referenced in 38 articles [sw03709]
  • systems. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic ... natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which ... hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements ... automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity...
  • HyTech

  • Referenced in 320 articles [sw04125]
  • hybrid system satisfies a temporal requirement. Hybrid systems are specified as collections of automata with ... verified by symbolic model checking. If the verification fails, then HyTech generates a diagnostic error...
  • HSolver

  • Referenced in 39 articles [sw07419]
  • HSolver is a program for verification of hybrid systems based on the constraint solver RSOLVER...
  • Benchmarks

  • Referenced in 23 articles [sw04612]
  • Safety verification of hybrid systems by constraint propagation based abstraction refinement This paper deals with ... problem of safety verification of non-linear hybrid systems. We start from a classical method...
  • STeP

  • Referenced in 36 articles [sw17948]
  • hybrid systems based on their temporal specification. Unlike most systems for temporal verification, STeP...
  • PPL

  • Referenced in 89 articles [sw05357]
  • employed in several systems for the analysis and verification of hardware and software components. Current ... synchronization protocols, real-time and hybrid systems. Since the seminal work of P. Cousot...
  • Breach

  • Referenced in 17 articles [sw20822]
  • Breach, a toolbox for verification and parameter synthesis of hybrid systems. We describe Breach...
  • DISCOVERER

  • Referenced in 40 articles [sw07719]
  • Based on the work of complete discrimination systems of polynomials [33,31],, we invented ... both on SAS-solving and program verification with DISCOVERER, and then discuss the future work ... programs, and reachability computation of hybrid systems...
  • HYSDEL

  • Referenced in 37 articles [sw05200]
  • propositional logic rules. Once a hybrid system is modeled in a human-readable fashion, HYSDEL ... optimization, to solve, e.g., optimal control, safety verification, or estimation and fault detection problems...
  • SPeeDI

  • Referenced in 7 articles [sw00896]
  • SPeeDI -- a verification tool for polygonal hybrid systems Hybrid systems combining discrete and continuous dynamics ... most nontrivial subclasses of hybrid systems this and all interesting verification problems are undecidable. Most ... case for classes of rectangular automata and hybrid automata with linear vector fields. Most implemented ... geometric properties of the specific (class of) systems under analysis. An interesting and still decidable...
  • STRONG

  • Referenced in 2 articles [sw19505]
  • STRONG: A Trajectory-Based Verification Toolbox for Hybrid Systems ... present STRONG, a MATLAB toolbox for hybrid system verification. The toolbox addresses the problem...
  • Bellerophon

  • Referenced in 1 article [sw23943]
  • control with physical motion. Verification is undecidable for hybrid systems and challenging for many models ... tactics language and library for hybrid systems verification, named Bellerophon, that provides ... focusing on the important domain of hybrid systems verification, Bellerophon emerges with unique automation that ... decomposing hybrid systems, discovering and establishing invariants of nonlinear continuous systems, arithmetic simplifications to maximize...
  • UniForM

  • Referenced in 8 articles [sw10332]
  • development of hybrid, real-time or reactive systems, transformation, verification, validation and testing. Moreover...
  • nuXmv

  • Referenced in 17 articles [sw18526]
  • verification algorithms. For infinite-state systems, it extends the nuXmv language with new data types ... been used in several industrial projects as verification back-end, and it is the basis ... contract based design, model checking of hybrid systems, safety assessment, and software model checking...
  • Stabhyli

  • Referenced in 4 articles [sw20122]
  • tool for automatic stability verification of non-linear hybrid systems. We present Stabhyli, a tool...
  • C2e2

  • Referenced in 7 articles [sw20139]
  • C2e2: A verification tool for stateflow models. Compare Execute Check Engine (C2E2) is a tool ... verifying bounded-time invariant properties of hybrid system and Stateflow models. It supports nonlinear dynamics...
  • JBernstein

  • Referenced in 2 articles [sw19486]
  • essential in many automated verification and synthesis tasks for hybrid systems, control algorithms, digital signal ... mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures...
  • 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...