Quicksort Verified by SPARK

This technical paper details the successful implementation and full functional verification (Platinum level) of the Quicksort algorithm using Ada and SPARK. Authored by David Easterling of the University of Dayton Research Institute, the study demonstrates how automatic verification tools can guarantee the logic and safety of complex autonomous applications.