Masterthesis: Static Type Checking of Regular Expression Types using SMT

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.

Desirable Skills

  • Interest in compiler design and type systems
  • Lecture SLE
  • Knowledge regarding SMT desired

Contact

For more information please sent your application documents to Flo Drux.

Prof. Dr. Bernhard Rumpe
Lehrstuhl Software Engineering
Ahornstr. 55
52074 Aachen