Shinya Umeno

I am a PhD candidate in the Computer Science and Artificial Intelligence Laboratory (CSAIL) at MIT. I am a member of the Theory of Distributed Systems (TDS) Group, led by Prof. Nancy Lynch.

My research interest is to develop techniques and software tools for producing reliable software/hardware systems. I am especially interested in checking mathematically provable correctness (formal verification) of concurrent/distributed real-time systems.

Currently I am working on developing novel abstraction techniques for time-parametric real-time system verification by focusing on event orders that are guaranteed by timing constraints on the underlying system's behavior. The main purpose of doing this abstraction is that instead of having continuously evolving variables such as clocks, the user can make use of event order information in system executions to construct untimed abstraction of the original timed model. The user can then use a conventional model-checker for untimed state-transition systems to automatically verify desirable safety properties of the system.