In most programming languages, amongst other things, type checking is used to find programming errors by limiting the values that can be assigned to specific variables. Regular expression types consist of a regular expression pattern that matches set of character sequences. The only accepted values of a regular expression type are those character sequences that match the pattern. This is useful to, e.g., assure safety of queries in the internet-of-things.
To statically type check regular expression types, a solution for the inclusion problem for regular expressions is required, which is PSPACE-complete. SMT (satisfiability modulo theories) solvers can be used to solve the inclusion problem for a subset of regular expressions in a short amount of time. Additionally, current solutions, be it algorithmic or software, do not handle all regular expressions offered by many modern matching engines; Extended regular expressions contain variables and whether they can be converted to regular expressions without variables is undecidable.
Within this thesis, the aim is to develop a type checker extension to type check a subset of regular expression types using an SMT solver. First and foremost, this requires a solution for the inclusion problem. The abstract syntax tree-visitors of the type checker are to be extended accordingly.
Tasks of this thesis
- Evaluate the MontiCore regular expression language and create a classification of whether regular expressions can be type checked (decidability).
- Create a normalization (or de-sugaring) solution for regular expressions (without variables).
- Create type check components to type check regular expression types.
- Create test data.
- Evaluate the approach.
- Interest in compiler design and type systems
- Lecture SLE
- Knowledge regarding SMT desired
For more information please sent your application documents to Flo Drux.
Prof. Dr. Bernhard Rumpe
Lehrstuhl Software Engineering