Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (Extended Version)

TL;DR

This paper extends abstract interpretation for hybrid systems by incorporating nonstandard analysis with infinitesimals, enabling scalable and rigorous verification of continuous dynamics modeled by ODEs.

Contribution

It introduces a novel approach combining NSA and abstract interpretation to improve the scalability and rigor of hybrid system verification.

Findings

Prototype successfully verifies benchmark examples.

Ensures soundness and termination with uniform widening operators.

Extends deductive verification for hybrid systems using infinitesimals.

Abstract

We extend abstract interpretation for the purpose of verifying hybrid systems. Abstraction has been playing an important role in many verification methodologies for hybrid systems, but some special care is needed for abstraction of continuous dynamics defined by ODEs. We apply Cousot and Cousot's framework of abstract interpretation to hybrid systems, almost as it is, by regarding continuous dynamics as an infinite iteration of infinitesimal discrete jumps. This extension follows the recent line of work by Suenaga, Hasuo and Sekine, where deductive verification is extended for hybrid systems by 1) introducing a constant dt for an infinitesimal value; and 2) employing Robinson's nonstandard analysis (NSA) to define mathematically rigorous semantics. Our theoretical results include soundness and termination via uniform widening operators; and our prototype implementation successfully verifies some benchmark examples.