The Airborne Information for Lateral Spacing (AILS) program at NASA Langley Research Center aims at giving pilots the information necessary to make independent approaches to parallel runways with spacing down to 2500 feet in Instrument Meteorological Conditions. The AILS concept consists of accurate traffic information visible on the navigation display and an alerting algorithm which warns the crew when one of the aircraft involved in a parallel landing is diverting from its intended flight path. In this paper we present a model of aircraft approaches to parallel runways. Based on this model, we analyze the alerting algorithm with the objective of verifying its correctness. The formalization is conducted in the general verification system PVS.