@inbook{d0a0c4420bb544c1a93b252be11f6115,
title = "Assume-guarantee abstraction refinement meets hybrid systems",
abstract = "Compositional verification techniques in the assumeguarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions we introduce an abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata.",
author = "Sergiy Bogomolov and Goran Frehse and Marius Greitschus and Radu Grosu and Corina Pasareanu and Andreas Podelski and Thomas Strump",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2014.",
year = "2014",
doi = "10.1007/978-3-319-13338-6_10",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "116--131",
editor = "Eran Yahav",
booktitle = "Hardware and Software",
address = "Germany",
}