Demo May 2017 You can download the latest demo here. Instructions to compile, run and visualize are included. The demo requires Linux or Mac. In case invariant.key cannot be loaded in KeY-ABS, run the latest model without traits (available here).