88 citations · 339 across the 67 of their papers we have counts for
5 papers · 1 filter
Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (Extended Version)
Kengo Kido, Swarat Chaudhuri, Ichiro Hasuo
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,…
Lattice-Theoretic Progress Measures and Coalgebraic Model Checking (with Appendices)
Ichiro Hasuo, Shunsuke Shimizu, Corina Cirstea
In the context of formal verification in general and model checking in particular, parity games serve as a mighty vehicle: many problems are encoded as parity games, which are then…
Time Robustness in MTL and Expressivity in Hybrid System Falsification (Extended Version)
Takumi Akazaki, Ichiro Hasuo
Building on the work by Fainekos and Pappas and the one by Donze and Maler, we introduce AvSTL, an extension of metric interval temporal logic by averaged temporal operators. Its e…
Coalgebraic Infinite Traces and Kleisli Simulations
Natsuki Urabe, Ichiro Hasuo
Kleisli simulation is a categorical notion introduced by Hasuo to verify finite trace inclusion. They allow us to give definitions of forward and backward simulation for various ty…
Input Synthesis for Sampled Data Systems by Program Logic
Takumi Akazaki, Ichiro Hasuo, Kohei Suenaga
Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturb…