IMDEA Software Institute faculty member Aleks Nanevski receives a prestigious ERC Consolidator Grant for the project "Mathador - Type and Proof Structures for Concurrent Software Verification".
Concurrent programs are notoriously difficult to write because of the complexity of interaction between their components. This complexity comes into the sharpest focus if one tries to develop a mathematical, computer-checkable, proof that a concurrent program produces the desired result. The required effort for developing such a proof today is overwhelming even for the simplest concurrent programs, because of the combinatorial explosion associated with the component interaction.
The goal of the Mathador project is to study, decompose, and simplify the structure of mathematical proofs of concurrent programs, to the point where they can be developed on a regular basis. Mastering these proofs will mean that we know how to describe the interaction between concurrent components in an intellectually manageable way. In turn, this will directly impact how we think about, write, and understand concurrent software.
More information: ERC Press Release, and List of ERC Consolidator Grant Awardees.