Exercises in Nonstandard Static Analysis of Hybrid Systems

Abstract. 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.

• Type: Journal
• Year: 2012
• Where: CAV
• Authors: Ichiro Hasuo, Kohei Suenaga
• Keywords: CAV 2012, Hardware, Hoare Logic, Hybrid Applications, Static Analysis Techniques