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).

Paper (extended version; a shorter version appeared in Proceedings of ESOP 2013)
RTRecS (Model Checker for mu-HORS)

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 twofiles.java, 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:

G1: (mu-HORS code)
G2: (mu-HORS code)
Thread: (mu-HORS code)
Thread2: (mu-HORS code)
Pred: (FJ source code) (mu-HORS code)
Ski1: (FJ source code) (mu-HORS code)
Ski2: (FJ source code) (mu-HORS code)
L-append: (FJ source code) (mu-HORS code)
L-map: (FJ source code) (mu-HORS code)
L-app-map: (FJ source code) (mu-HORS code)
L-even: (FJ source code) (mu-HORS code)
L-filter: (FJ source code) (mu-HORS code)
L-risers: (FJ source code) (mu-HORS code)
Twofiles: (FJ source code) (mu-HORS code)