Petr Cermak, a final-year MEng undergraduate student, has been awarded a perfect score of 100% for his final-year individual project.

A number of DoC students in the past have produced exceptional individual projects that have been awarded in excess of 90% but this is the first time in the Department’s history that a student has been awarded 100%.

Petr’s project explores the gap between game theory, which models the way individuals form strategies for maximizing profit, and model checking, which establishes whether or not a given property, expressed in formal mathematical logic, holds in a system modeled as a finite state-state automaton.  Petr identified two diverse variants of strategy logic and devised and implemented symbolic model checking algorithms for them, developing formal time and space complexity analyses and correctness proofs for each.  “What interested me about the project was the fact that I could work on something that had never been done before. I was intrigued by the challenge of the unknown and the potential to contribute something to computer science. I achieved this by building the first tool that supports Strategy Logic verification. The tool also provides strategy synthesis, which could be used one day to generate computer programs automatically. It felt very rewarding to have our paper accepted at a top conference.”

Petr was one of eight prize candidates who re-presented their project work at the Department’s “Prize Finalists” event on June 26^th and was voted the best project in an informal poll of the attendees.  The prize committee awarded Petr the Governors’ Prize as the top graduating MEng student in Computing and the IBM Project Prize for his final-year project.

His supervisor, Prof. Alessio Lomuscio, an expert on verification and multi-agent systems, said that "the scientific results Petr obtained are very significant in breadth and depth; they are comfortably at the level of the top research presented at the most prestigious conferences in verification”. He added: “Overall, this is truly an outstanding undergraduate project, certainly the most significant one I have seen in the past 15 years as an academic”.

The first two months of the project, which began in early November 2013, led to a paper that was accepted at the top international conference on computer-aided verification (CAV 2014).  Petr  presented the paper, “MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications”, in Vienna on July 21^st.

Petr’s subsequent work is the subject of a second paper, currently in preparation, that Prof. Lomuscio is especially excited about: “I judge this result worthy of a very significant paper (considerably deeper than the CAV2014 paper) on its own. I am astonished that Petr was able to achieve these results in such a short time whole at the same time attending undergraduate courses.”

One of the Department’s external examiners, Prof. John Gurd, congratulated the Department for being able to foster such a remarkable talent and for having the courage to award 100% for a piece of work that simply could not be bettered under the circumstances.

After completing the current paper, Petr plans to spend the rest of the summer in his home town of Velká Dobrá near Prague before returning to London in September, where he will be working for Google.  He may yet decide to do a PhD.

Petr’s report has been published as one of the Computing Department’s “Distinguished Projects” for 2014 and can be found here: //www3.imperial.ac.uk/computing/teaching/ug/ug-distinguished-projects.