Language-Based Abstraction Refinement for Hybrid System Verification

DOI10.1007/978-3-540-69738-1_11zbMATH Open1132.68471OpenAlexW1576022414MaRDI QIDQ5452604FDOQ5452604

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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
• Title not available (Why is that?)

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)