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.
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.
- Winter Semester 2015/2016:
Albert Rizaldi, Fabian Immler, and Matthias Althoff.
A formally verified checker of the safe distance traffic rules for
In NASA Formal Methods - 8th International Symposium, NFM
2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings, pages 175-190,
[ DOI |
D. Han, A. Rizaldi, A. El-Guindy, and M. Althoff.
On enlarging backward reachable sets via zonotopic set membership.
In Proceedings of the IEEE International Symposium on
Intelligent Control, 2016.
[ .bib |
A. Rizaldi, S. Söntges, and M. Althoff.
On time-memory trade-off for collision detection.
In Proc. of the IEEE Intelligent Vehicles Symposium, 2015.
[ .bib |
A. Rizaldi and M. Althoff.
Formalising traffic rules for accountability of autonomous vehicles.
In Proc. of the 18th IEEE International Conference on
Intelligent Transportation Systems, 2015.
[ .bib |