Apr 12, 2011: Alfons Laarman: Multi-Core LTSmin: Marrying Modularity and Scalability

April 12, 2011Multi-Core LTSmin: Marrying Modularity and Scalability
Room: Zi 5126Alfons Laarman

The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral speci cations (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 effciency and memory usage: low overhead load balancing, incremental hashing and scalable state compression.