For performing advanced analyses on models, AF3 makes use of external specialized tools. Currently we use NuSMV for performing model checking and Yices for lightweighted non-determinism analyses for state automata. Information about installing these tools are here .
The collection screencasts and presentations provide a quick overview of the main features of AF3.
Watch them to learn how to get started with AF3. Most screencasts are 2 to 5 minutes long.