Main Features:

Integrated modeling of the application software up to the platform

Support for validation and verification

Support for efficient deployments







Download for Free:

Runs on...

AF3 2.5


AF3 2.x ("Nightly Build")


Integrated Provers:

For performing advanced formal analyses on models, AF3 makes use of external specialized tools. Currently we use NuSMV and CBMC for performing model checking and Z3 and Yices for lightweighted non-determinism analyses for state automata. Information about installing these tools are here .


Learn Online:

The of screencasts and presentations provide a quick overview of the main features of AutoFOCUS3. Watch them to learn how to get started with AutoFOCUS3. Most screencasts are 2 to 5 minutes long.