Formal Verification Made Easy

FASTEN is an open source environment for the formal specfication and verification of systems. It uses JetBrains' Meta Programming System to build a set of DSLs on top of the input language of NuSMV

FASTEN offers modern tool support for editing models and interacting with NuSMV. Common usage patterns of NuSMV are lifted as first class DSLs which can be freely combined with each other. From the models, we generate .smv text files on which NuSMV is run and the results are lifted back in the IDE.


FASTEN at a Glance