The logician Patrick Blackburn proposed several times to consider modal formulas as automata that are placed at some point inside a relational model and explore their environment by making transitions to accessible points on their own. This project realizes this idea and considers modal formulas as computer programs. Therefore, an interpreter and an incrementally extensible compiler conforming to the standard translation of the correspondence theory are implemented. Translating modal programs into executable computer programs that are able to evaluate their validity independently in every environment, this compiler turns out to be a very fast and extremely flexibly applicable model checker.
Oracle Academy: Award of $5,000 for outstanding project in the systems software category.