From Language Workbenches to Verification Workbenches

From Language Workbenches to Verification Workbenches
Master Project

Thesis

https://resolver.tudelft.nl/uuid:0a13ca4a-9d3c-416e-bb88-affc3f14ee52

Problem statement

Software verification is an essential part of building highly reliable software, yet powerful and user-friendly tools for software verification are currently rare and building new ones is an arduous and complex task. Language workbenches such as Spoofax could be used to greatly reduce the cost of new such tools, but current state-of-the-art workbenches lack essential features to do this in practice. In particular, the Statix meta-language for specifying type systems does not yet support essential features such as type-level computation and higher-order unification. Hence a currently open problem is how to build a language workbench for software verification.

Project description

The goal of this project is to contribute towards making language workbenches better suited for the task of implementing not just programming languages but verification languages. In particular, some concrete objectives could be:

Extending Statix (or another constraint-based language) with new primitives for expressing type-level computation.
Extending Statix (or another constraint-based language) with new primitives for elaboration of implicit arguments.
Extending Statix (or another constraint-based language) with new primitives for expressing higher-order unification.
Extending Statix (or another constraint-based language) with new primitives for expressing meta-programs such as tactics.
Investigating strategies for compiling and optimizing specifications of verification languages written in Statix.