When used properly, FDR is capable of verifying systems with billions (even trillions of states, if a cluster is being used) of explicit states. This section explains the different ways in which scripts can be optimised to take full advantage of FDR, whilst also explaining how to best configure and setup FDR to check a given problem.

This section assumes that you have an extremely large check that you wish to perform, but are unable to do so on your standard computer.