• HyTech

  • Referenced in 321 articles [sw04125]
  • linear hybrid system satisfies a temporal requirement. Hybrid systems are specified as collections of automata...
  • HYSDEL

  • Referenced in 37 articles [sw05200]
  • class of hybrid systems described by interconnections of linear dynamic systems, automata, if-then-else...
  • LinAIG

  • Referenced in 6 articles [sw10316]
  • Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces ... symbolic algorithm for the verification of linear hybrid automata with large discrete state spaces (where ... part and the continuous part of the hybrid state space are represented by one symbolic ... minimization: redundancy elimination eliminates so-called redundant linear constraints from LinAIG representations by a suitable...
  • BACH

  • Referenced in 4 articles [sw11906]
  • BACH: bounded reachability checker for linear hybrid automata. Hybrid automata are well studied formal models ... Even for the simple class of linear hybrid automata, the reachability problem is undecidable ... author’s previous work, for linear hybrid automata we proposed a linear programming based approach ... perform bounded reachability checking of linear hybrid automata. The experiment data shows that BACH...
  • HASL

  • Referenced in 6 articles [sw13330]
  • stochastic models. We introduce the Hybrid Automata Stochastic Logic (HASL), a new temporal logic formalism ... event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries to select prefixes...
  • COSMOS

  • Referenced in 5 articles [sw13329]
  • Automata Stochastic Logic (HASL). HASL employs Linear Hybrid Automata (LHA), a gen eralization of Deterministic...
  • SPeeDI

  • Referenced in 7 articles [sw00896]
  • classes of rectangular automata and hybrid automata with linear vector fields. Most implemented computational procedures ... interesting and still decidable class of hybrid system are the (two-dimensional) polygonal differential inclusions...
  • LySHA

  • Referenced in 3 articles [sw20150]
  • algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function...
  • FORTS

  • Referenced in 1 article [sw15029]
  • FORTS is a model checker on Linear Hybrid Automata (LHA) that I write...
  • SReach

  • Referenced in 4 articles [sw20158]
  • uncertainty. The second one is probabilistic hybrid automata with additional randomness for both transition probabilities ... Standard approaches to reachability problems for linear hybrid systems require numerical solutions for large optimization...
  • CAR30

  • Referenced in 3 articles [sw08370]
  • Cellular Automata (CA) along with a Maximum Length Linear Hybrid CA. This design...
  • CalCS

  • Referenced in 6 articles [sw13098]
  • satisfiability solving of Boolean combinations of non-linear constraints that are convex. Our approach applies ... generated from bounded model checking of hybrid automata and static analysis of floating-point software...
  • REDLIB

  • Referenced in 5 articles [sw21175]
  • full TCTL model-checking of dense-time automata with multiple fairness assumptions. REDLIB uses ... fixpoint calculation, parametric safety analysis of linear hybrid systems, speed-up techniques for greatest fixpoint...
  • HyLAA

  • Referenced in 2 articles [sw20821]
  • tool for computing simulation-equivalent reachability for linear systems. Simulations are a practical method ... that can be reached using a particular hybrid automaton simulation algorithm, a property we call ... tool for simulation-equivalent reachability for hybrid automata with affine dynamics. HyLAA’s analysis ... unsafe state if and only if the hybrid automaton simulation engine could produce such...
  • ATLAS

  • Referenced in 195 articles [sw00056]
  • This paper describes the Automatically Tuned Linear Algebra...
  • CGAL

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

  • Referenced in 1758 articles [sw00161]
  • Coq is a formal proof management system. It...
  • GAP

  • Referenced in 2735 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • gmp

  • Referenced in 260 articles [sw00363]
  • GMP is a free library for arbitrary precision...
  • Isabelle

  • Referenced in 601 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...