kein Bild

M.Sc. Albert Rizaldi

Curriculum Vitae

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.


  • 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


  • Rizaldi, Albert; Keinholz, Jonas; Huber, Monika; Feldle, Jochen; Immler, Fabian; Althoff, Matthias; Hilgendorf, Eric; Nipkow, Tobias: Formalising and Monitoring Traffic Rules for Autonomous Vehicles Involving Multiple Lanes in {Isabelle/HOL}. Proc. of the 13th International Conference on integrated Formal Methods, 2017accepted mehr…
  • Han, D.; Rizaldi, A.; El-Guindy, A.; Althoff, M.: On Enlarging the Backward Reachable Sets via Zonotopic Set Membership. IEEE Multi-Conference on Systems and Control, 2016 mehr…
  • Rizaldi, A.; Söntges, S.; Althoff, M.: On Time-Memory Trade-Off for Collision Detection. Proc. of the IEEE Intelligent Vehicles Symposium, 2015 mehr…
  • Rizaldi, A.; Althoff, M.: Formalising Traffic Rules for Accountability of Autonomous Vehicles. Proc. of the 18th IEEE International Conference on Intelligent Transportation Systems, 2015 mehr…