Symbad: a Symbolic Executor of Sequential Ada Programs