SPARK—an annotated Ada subset for safety-critical programming | Proceedings of the conference on TRI-ADA '90
https://dl.acm.org/doi/10.1145/255471.255563
https://doi.org/10.1145/255471.255563