Model-Checking Higher-Order Programs with Recursive Types

This page provides information about our work on model-checking of higher-order programs with recursive types, and its applications to a software model checker for FJ (Featherweight Java).

You can test our model checker for FJ (combination of a translator FJ2HORS from FJ to mu-HORS, and a model checker RTrecS for mu-HORS). Enter a FJ program in the box below, and press the "submit" button. It checks that the program does not fail (specified by a special global action "fail") nor cause "message not understood" errors. (Among the examples above, you cannot test, as you need to write a property-automaton by yourself and pass it to RTrecS.) The underlying model checker RTRecS can be tested here. You can check only small examples as the time-out is set to one second.

Programs used in the experiments in the draft paper above: