Date of Award
Master of Science in Electrical Engineering
Department of Electrical and Computer Engineering
Kenneth M. Hopkinson, PhD
The software verification in this thesis concentrates on verifying a particle filter for use in tracking and estimation, a key application area for the Air Force. The development and verification process described in this thesis is a demonstration of the power, limitation, and compromises involved in applying automated software verification tools to critical embedded software applications.
DTIC Accession Number
Terry, Osiris J., "Formal SPARK Verification of Various Resampling Methods in Particle Filters" (2022). Theses and Dissertations. 5370.