Hunt, Warren A., 1958-2011-08-192011-08-192007-05http://hdl.handle.net/2152/13244textThis dissertation discusses the application of formal verification methods to reasoning about the correctness of computer controlled systems. Due to the switching that is introduced by the computer controller, the differential equations associated with such systems may consist of discontinuous vector fields. The physical system may also experience switching due to physical interaction, such as impact. Such system models may exhibit an infinite number of switches in finite time. For example, using rigid body modeling assumptions, a bouncing ball may have infinitely many elastic impacts, but come to rest in finite time. Using nonstandard analysis, we present a model for computer controlled systems which accommodates discontinuous vector fields as well as infinite switches in finite time. This model includes both the semantics of the computer program as well as the ordinary differential equations governing the physical system behavior. We develop a nonstandard definition of a solution for such a model and formally prove that the solution exists. Using this nonstandard definition of solution, we develop proof procedures whereby one may reason about safety and progress properties of the system. The soundness of these proof procedures is formally shown. We conclude with the presentation of a simple example computer controlled system using the presented model, for which safety and progress properties are shown using the respective proof procedures.electronicengCopyright is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works.Computer programs--VerificationAutomatic control