Counterexample-guided predicate abstraction of hybrid systems

DOI10.1016/j.tcs.2005.11.026zbMath1088.68096OpenAlexW1793594870WikidataQ124832924 ScholiaQ124832924MaRDI QIDQ2368954

Rajeev Alur, Thao Dang, Franjo Ivančić

Publication date: 28 April 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.11.026

zbMATH Keywords

Hybrid systemsModel checkingVerificationPredicate abstractionCounterexample analysis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (15)

Template-Based Unbounded Time Verification of Affine Hybrid Automata ⋮ Verification of Hybrid Systems ⋮ An Introduction to the Verification of Hybrid Systems Using Ariadne ⋮ Formal Verification Applied to Robotic Surgery ⋮ Hybridization methods for the analysis of nonlinear systems ⋮ Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems ⋮ Extracting counterexamples induced by safety violation in linear hybrid systems ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ Abstractions Refinement for Hybrid Systems Diagnosability Analysis ⋮ An approximation algorithm for box abstraction of transition systems on real state spaces ⋮ Computing reachable states for nonlinear biological models ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ Symbolic Model Checking of Hybrid Systems Using Template Polyhedra ⋮ Hybrid systems: From verification to falsification by combining motion planning and discrete search ⋮ Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers

Uses Software

• cdd
• Kronos
• SPIN
• HyTech
• Qhull
• Uppaal
• Bandera
• Bebop

Cites Work

• The algorithmic analysis of hybrid systems
• Minimum polygonal separation
• On the complexity of polyhedral separability
• A theory of timed automata
• Property preserving abstractions for the verification of concurrent systems
• Timing verification by successive approximation
• The quickhull algorithm for convex hulls
• Lazy abstraction
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Counterexample-guided predicate abstraction of hybrid systems