Date and Time: Thursday, 22 December 2011, 15:45 - 16:45

Location: HG 6.96

Speaker: Jaco van de Pol (Formal Methods and Tools, University of Twente)

Title: Recent progress on the LTSmin toolset

Abstract:

I will give an overview on the latest developments in the LTSmin toolset. LTSmin is a tool for high-performance model checking, with three main engines: distributed, multi-core and symbolic reachability. The tool can detect deadlocks and safety or liveness violations on-the-fly, and provides full symbolic mu-calculus model checking. LTSmin is language independent. Through the PINS interface, the verification engines can be linked to existing languages by language modules. Such modules exist for prominent modelling languages, like mCRL2 and PROMELA. The focus of the talk will be on the recent multi-core algorithm for LTL model checking based on Nested Depth-First Search, and on the implementation of partial-order reduction as a language-independent building block.