Practical Application of SPARK to OpenUxAS. - M. Anthony Aiello; Claire Dross; Patrick Rogers; Laura R. Humphrey; James Hamil (FM, 2019)

End-to-End Verification of Initial and Transition Properties of GR(1) Designs in SPARK. - Laura R. Humphrey; James Hamil; Joffrey Huguet (SEFM, 2020)