Multi-Core LTSmin: Marrying Modularity and Scalability

The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression