In formal verification of hybrid systems, a big challenge is to incorporate continuous flow dynamics in a discrete framework. Our previous work proposed to use nonstandard analysis (NSA) as a vehicle from discrete to hybrid; and to verify hybrid systems using a Hoare logic. In this paper we aim to exemplify the potential of our approach, through transferring static analysis techniques to hybrid applications. The transfer is routine via the transfer principle in NSA. The techniques are implemented in our prototype automatic precondition generator. © 2012 Springer-Verlag.
CITATION STYLE
Hasuo, I., & Suenaga, K. (2012). Exercises in nonstandard static analysis of hybrid systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 462–478). https://doi.org/10.1007/978-3-642-31424-7_34
Mendeley helps you to discover research relevant for your work.