by Justin Holmgren
—
I’m wearing the shirt with circles on it
This summer I did a research internship at the newly established Hasuo Lab in the Department of Computer Science at the University of Tokyo. This lab’s research centers on the use of particularly abstract mathematics to study formal logic in computer science. This internship was organized by MIT’s MISTI‐Japan Program and supported by Friends of UTokyo Inc.
My internship was about the formal verification of hybrid systems. Hybrid systems are systems in which some continuous evolving behavior is combined with some discrete controlling behavior, in contrast to typical software verification, which involves only the latter. The archetypal example of a hybrid system is train or aircraft control, with collision-free operation the desired behavior, but many other examples abound in numerous fields from biology to economics.
The original goal for my internship was to investigate the applicability of nonstandard analysis in transferring software verification techniques to hybrid systems. Nonstandard analysis is a branch of analysis which extends the real numbers to the hyperreals, a field which also includes infinitesimals, thus forming a natural system for describing continuous motion. One of the main results of nonstandard analysis is a transfer principle which roughly states that any true statement about the reals has an analogous true statement about the hyperreals. The basic idea of our theoretical framework was to augment a normal imperative programming language with an infinitesimal constant dt. Using this fact, I attempted to apply state of the art software verification techniques to our framework for hybrid system verification.
Kiyomizu Temple in Kyoto
Unfortunately, there were many problematic subtleties. For example, while one can use polyhedral abstract interpretation, an arbitrary interval must be used for the initial value of dt, which generally immediately makes the strategy too weak. Furthermore, in precondition generation, many different preconditions imply the given postcondition. The conventional methods’ heuristics do not target preconditions which make use of dt’s infinitesimality. I ended up implementing a template-based precondition generator in Mathematica using which was able to overcome some of these difficulties.
Outside of work, I had a great time exploring Japan with my fellow MIT students. Japan is such a unique place – I enjoyed various themed cafes, as well as ordinary izakayas and onsens.
