Mohammad Abdulaziz email: firstname.lastname@example.org
Since May 2017 I am a post-doc in the Chair for Logic and Verification in the Technical University of Munich, which is led by Prof. Tobias Nipkow.
My research concerns problems that I find interesting, and whose solution can help produce provably safe AI systems, and software systems in general.
I currently have two main research activities:
- I develop new algorithms for solving problems in transition systems, and formally verify them in the interactive theorem provers HOL4 and Isabelle/HOL. The main application for these algorithms is in AI planning. I worked on algorithms for symmetry breaking and upper-bounding state-space diameters, and a verified plan validators for PDDL.
- A more foundational side of my work involves formalising pure mathematics in Isabelle/HOL, with a focus on analysis and differential geometry.
I am working on different variants of Stokes' theorem.
Until now, together with Prof. Larry Paulson, we developed the first formalisation of Green's theorem.
For my PhD (which is to be conferred by the end of 2017), I studied at the Australian National University and Data61 under the supervision of Dr. Michael Norrish and Dr. Charles Gretton, where I worked on verifying algorithms for transition systems in the proof assistant HOL4.
Before that I obtained an MSc and a BSc in Computer Engineering from Cairo University in 2009 and 2013, respectively, under the supervision of Prof. Amr Wassal and Prof. Nevine Darwish. I also worked from 2011 to 2013 as a software engineer in Mentor Graphics developing CAD tools for Custom ICs, and as a systems engineer in Cairo University developing FPGA based communication systems from 2009 to 2011.
For more details, please refer to my CV.
Mohammad Abdulaziz, Michael Norrish, and Charles Gretton. Formally Verified Algorithms for Upper Bounding State Space Diameters. Submitted for Review to the Journal of Automated Reasoning. [PDF]
Mohammad Abdulaziz and Lawrence C Paulson. An Isabelle/HOL Formalisation of Green's Theorem. Submitted for Review to the Journal of Automated Reasoning. [PDF]
Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. A State Space Acyclicity Property for
Exponentially Tighter Plan Length Bounds. In International Conference on Automated Planning and
Scheduling (ICAPS). In Press, 2017. [PDF]
Mohammad Abdulaziz and Lawrence C. Paulson. An Isabelle/HOL Formalisation of Green's Theorem.
In International Conference on Interactive Theorem Proving, pages 3-19. Springer, 2016. [PDF]
Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. Verified Over-Approximation of the
Diameter of Propositionally Factored Transition Systems. In International Conference on Interactive
Theorem Proving, pages 1-16. Springer, 2015. [PDF]
Mohammad Abdulaziz, Michael Norrish, and Charles Gretton. Exploiting Symmetries by Planning for a Descriptive Quotient. In International Joint Conference on Artificial Intelligence, IJCAI, pages 25-31, 2015. [PDF]
Sherif M Saif, Mohamed Dessouky, Salwa Nassar, Hazem Abbas, M Watheq El-Kharashi, and Mohammad Abdulaziz. Exploiting Satisfiability Modulo Theories for Analog Layout Automation. In International Design and Test Symposium (IDT), pages 1-6. IEEE, 2014.
Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. Mechanising Theoretical Upper Bounds
in Planning. In Workshop on Knowledge Engineering for Planning and Scheduling, 2014. [PDF]
Mohammad Abdulaziz, Ahmed Ramadan, and Sherif Saif. An SMT Based Electrical and Geometrical
Constraint Solving Paradigm. In Mentor Graphics Innovation Workshop, Cairo, Egypt, 2012.
Mohammad Abdul Aziz, Amr Wassal, and Nevine Darwish. A machine learning technique for hardness
estimation of QFBV SMT problems (work in progress). In International Workshop on Satisfiability
Modulo Theories, 2012. [PDF]