Researchers at King's and the University of Illinois at Urbana-Champaign (UIUC) are collaborating to develop techniques to enhance software verification environments, to simplify the verification of high-level programming languages.
An important component of the verification process is the management of names and name-binding. The standard approach is to replace names with numerical codes known as de Bruijn indices. While this avoids some of the difficulties of reasoning about names in programs, conducting a formalisation in de Bruijn style is labour-intensive and imposes a significant overhead to comprehending and reusing proofs. Nominal techniques offer an alternative, user-friendly approach, which does not require to replace names with codes.
The research collaboration between King's and UIUC seeks to combine nominal techniques with verification frameworks in order to simplify software verification. Professor Maribel Fernandez, Professor of Computer Science at King's Department of Informatics, elaborated further:
"In this project, we aim to apply novel nominal techniques to simplify the handling of names and binders in current verification tasks, such as verification of blockchain languages. Based on recent advances in nominal specification techniques by the King's team, we plan to develop a core nominal calculus, which will serve as a basis to enrich with nominal features two successful verification frameworks developed by the Illinois team: Maude and K. Our long term goal is to obtain nominal extensions of Maude and K. This ambitious goal will require both novel ideas and engineering effort. This project is a first, necessary step, and will make our long-term goal achievable by combining the complementary expertise of the teams in London and Illinois."– Professor Maribel Fernandez
This research is supported by a two-year Royal Society International Exchanges Grant, which is awarded to stimulate collaborations between scientists based in the UK and leading scientists overseas.
