SPARK - an annotated Ada subset for safety-critical programming. - Bernard Carré; Johnathan Randall Garnsworthy (TRI-Ada, 1990)

Fundamental concepts for fault tolerant systems. - Johnathan Randall Garnsworthy (1990)