author: Daan van Beek
title: Comparing the LTSmin and NuSMV reachability tools via automatic translation of their respective input languages
keywords: Symbolic Model Checking, LTSmin, NuSMV, reachability
committee: Jaco van de Pol ,
Gijs Kant ,
Arend Rensink
started: February 2013
end: August 2013


In this thesis we:

  • Provide automatic translations from SMV to an LTSmin input language.
  • Formalize and prove these translations to be correct.
  • Use the translations to translate several SMV models to mCRL2 models and execute them on SMV and LTSmin in order to obtain experimental results.
  • Explain the results by using the theory behind the NuSMV and LTSmin reachability tools.


Additional Resources

  1. The paper