Apr 03, 2012: Ruben Oostinga: A Java Bridge for LTSMin

April 03, 2012A Java Bridge for LTSMin
Room: Zi 5126Ruben Oostinga

LTSmin is a model checker developed by FMT which tries to combine enumerative model checking with symbolic model checking. It is modular in its design. It has language modules which can load models specified in various modelling languages. Analysis algorithms can interface with these language modules to provide model validation.
However currently LTSmin is programmed in C and it not very easy for newcomers to add new modules. To resolve this issue a Java interface is being developed. This interface allows analysis algorithms implemented in Java to use the existing language modules. It also makes it possible to add new language modules implemented in Java which can be used with the existing analysis algorithms as well as the new Java algorithms.
This meeting will talk about various ways of bridging Java and C as well as the design and implementation of the Java bridge.