About me

I am a enthusiastic Computer Scientist, currently employed at Aalborg University as Tenure Track Assistant Professor.

My key interests are; automatic controller synthesis, optimization, verification and learning -- primarily focused on model-based techniques with a strong foundation in formal methods.

You can reach me by mail: root@petergjoel.dk or pgj@cs.aau.dk for matters related to my employment at the university.

My linkedin account found here and you will also find my on Twitter.

A lot of my software can be found under my Github profile.

A short CV

Professional career

2019 - ? : Tenure Track Assistant Professor at Aalborg University
2018 - 2019: Post Doc at Aalborg University
2014 - 2018: PhD student at Aalborg University


Aalborg University 2014-2018, PhD Efficient Analysis and Synthesis of Complex Quantitative Systems
Université libre de Bruxelles 2013-2014, five months of exchange during my masters
Aalborg University 2012-2014, Masters Degree in Computer Science
Aalborg University 2009-2012, Bachelors Degree in Computer Science
HTX Holstebro 2006-2009, Communication and IT
Gudenaadalens ungdomsskole 9th and 10th grade
Nr. Nissum folkeskole 0-8th grade

Academic profile

For a full list of publications, please refer to either Google Scholar, dblp or my university profile.


  • Co-supervision of +4 PhD students
  • (Co-)supervision of +10 Master Thesis projects
  • 3 Lectures on "Advanced Topics in Modeling and Verification"
  • Distributed Systems (Masters level), 2020-2021
  • Started the interactive exercise suite for Distributed Systems
  • Introduction to C, 2022
  • Co-lectured 2 PhD courses

Academic Community Service

Software & Projects

More projects can be found on my Github profile

Academic artefacts

My research often results in libraries, tools or extensions of existing projects. Below is a non-comprehensive list of my contributions.

  • The Timed Automata-based tool Uppaal, in particular the Uppaal Stratego branch for automatic (near optimal) controller synthesis.
  • The Timed-Arc Petri Net tool Tapaal, in particular the discrete-timed engine (verifydtapn) and the untimed engine (verifypn) for verification of CTL, LTL and controller synthesis.
  • The Pushdown Automata verification library PDAAAL used in the AALWINES tool for network verificaiton.

Non-academic software

As of 2013, I have released an Android and a iPhone app for finding shelter in the wild (Denmark only). The app is called Shelter and has been developed in colaboration with Nicolaj Skafsgaard.