Research Assistant

Curriculum Vitæ

I am PhD student under Prof. Dr.-Ing. Matthias Althoff since 2014. I completed my master degree in Erasmus Mundus programme Dependable Software Engineering (DESEM) in 2014. I spent my first and second year in Universite de Lorraine (UdL), France and University of St Andrews (StA), Scotland respectively. In UdL, I researched the problem of how we can model an insulin pump formally in Event-B specification system. In StA, I studied the foundation of action-based stochastic logic for Markov Automata. From 2011 to 2012, I was working as software engineer in Gemalto, Singapore. I also completed my bachelor degree in Electrical Engineering from Institut Teknologi Bandung, Indonesia in 2011.

Research Interests

I am doing my PhD under PUMA and my topic is mainly about formal verification of autonomous sytems in Isabelle theorem prover.

From a top-bottom perspective (Artificial Intelligence), I am currently researching about eliciting and formally specifying traffic rules, e.g. from the Vienna Convention, as a specification for self-driving cars. We believe that if a self-driving car always obeys traffic rules, it should not be held liable even during an accident. At the moment, I am inclined to use BDI logic for specifying the traffic rules. With this set of formalised traffic rules, we could design a planner in agent-oriented language to achieve a rational --- and formally verified --- agent.

From a bottom-up perspective (Cyber-Physical Systems), I am currently researching about a formally verified and executable temporal logic-based motion planner in Isabelle theorem prover. This research combines three different interpretations of `formal verification' i.e. reachability analysis, model checking, and theorem proving. A plan from this motion planner will not only be the sequence of discrete actions to perform, but also a physical controller in control theory sense --- both are formally verified.

In overall, I really like to do cross-disciplinary research (control theory, theorem proving, model checking, functional programming, multi-agent systems) so that we can have a full stack, formally verified implementation of autonomous systems.

Teaching

• Winter Semester 2015/2016:
  • Teaching Assistant for Artificial Intelligence, especially for the topics about Logical Agents.
  • Advisor for Cyber-Physical Systems Seminar on topic about Automated Theorem Proving for verifying Cyber-Physical Systems

Publications