--- res: bibo_abstract: - We study the reachability problem for hybrid automata. Automatic approaches, which attempt to construct the reachable region by symbolic execution, often do not terminate. In these cases, we require the user to guess the reachable region, and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata according to the theory in which their reachable region can be defined finitely. This is the theory in which the prover needs to operate in order to verify the guess. The approach is interesting, because an appropriate guess can often be deduced by extrapolating from the first few steps of symbolic execution.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Vlad foaf_name: Rusu, Vlad foaf_surname: Rusu bibo_doi: 10.1007/3-540-64358-3_40 bibo_volume: 1386 dct_date: 1998^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/9783540643586 dct_language: eng dct_publisher: Springer@ dct_title: Reachability verification for hybrid automata@ ...