Language-Based Abstraction Refinement for Hybrid System Verification

DOI10.1007/978-3-540-69738-1_11MaRDI QIDQ5452604zbMATH OpenOpenAlexFDO

Authors Felix Klaedtke, Stefan Ratschan, Zhikun She

Publication date 4 April 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69738-1_11

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1956581
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Hybrid Systems: Computation and Control
• Counterexample-guided predicate abstraction of hybrid systems
• Formal Methods in Computer-Aided Design

Cites work

• scientific article; zbMATH DE number 1794363 (Why is no real title available?)
• scientific article; zbMATH DE number 2090047 (Why is no real title available?)
• scientific article; zbMATH DE number 1424031 (Why is no real title available?)
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Comparing abstraction refinement algorithms
• Constraint propagation with interval labels
• Constraints for Continuous Reachability in the Verification of Hybrid Systems
• Counterexample-guided abstraction refinement for symbolic model checking
• Formal Modeling and Analysis of Timed Systems
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• MONA IMPLEMENTATION SECRETS
• On the expressiveness and decidability of o-minimal hybrid systems
• What's decidable about hybrid automata?

Cited in

(8)

• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• LMS-Verify: abstraction without regret for verified systems programming
• Hybrid Systems: Computation and Control
• Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models
• Hybrid automata-based CEGAR for rectangular hybrid systems
• Hybrid automata-based CEGAR for rectangular hybrid systems
• Hybridization based CEGAR for hybrid automata with affine dynamics
• scientific article; zbMATH DE number 1956581 (Why is no real title available?)

Describes a project that uses

Uses Software

• RAMAS

This page was built for publication: Language-Based Abstraction Refinement for Hybrid System Verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5452604)