This paper provides a brief overview of five projects in which Honeywell has successfully used or developed model checking
methods in the verification and synthesis of safety-critical systems.
This material is based in part upon work supported by Rome Labs (contract F30602- 00-C-0017), AFOSR (contract F49620-97-C-0008),
and NASA (cooperative agreement NCC-1-399)