Computer systems and automation are performing more and more important functions where mistakes can be very expensive or even life-threatening. This leads to a new perspective on how we treat an error in the computer code.

Jeremy Liang An Kong, winner of the VCLA International Student Award for Outstanding Master Thesis in Computer Science, provides us with an example where the explicit and implicit costs can be too dear.

,,For the Mars rover, a model checking tool determined that there was a bug in the file system, which is a key part of the operating system of the rover. If this wasn’t found, it’s possible that the operating system would have malfunctioned. Scientists could have lost control of the rover and/or the rover could otherwise cease to be operational – so this would have been a waste of the $1.5 billion that went into it!

Alternatively (and it’s difficult to put a price on this), a subtle bug in the rover could also mean that it looked like it worked, but it silently sent incorrect or corrupted information to the scientists monitoring it. This might not be noticeable until much later, meaning that much scientific investigation, time and resources might have been invested based on incorrect data.”- Jeremy Liang An Kong

The author in his thesis “MCMAS-Dynamic: Symbolic Model Checking Linear Dynamic Logic” under the supervision of Alessio Lomuscio, Imperial College London, builds on Linear Dynamic Logic (introduced by De Giacomo, Giuseppe and Moshe Vardi, at IJCAI 2013, Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence) and develops novel practical algorithm for LDL model checking, which is formally correct, allows symbolic implementation (used in other languages) and takes into consideration observational semantics and distributed common knowledge. Further on, his technique allows him to upgrade the MCMAS model checker to #MCMAS Dynamic extension, thus supporting a language which is more expressive.

Jeremy Liang An Kong is presented with the VCLA Certificate for the Outstanding Master Thesis and the voucher for the cash prize at the FLoC 2018 Olympic Games, in Oxford, by Dana Scott.

Listen to the presentation of Jeremy Liang An Kong, winner of the VCLA International Student Award for Outstanding Master Thesis 2018 on our YouTube channel here.

For more on annually Awarded VCLA International Student Awards click here.