Introduction Problems in a program's specification can undermine the trust obtained from verification. If the specification doesn't actually state what you intended it to state, the verification may still be technically sound but provide a false sense of security that the program behaves as intended. There are many ways that the text of a specification may differ from its intent, but there are some specific signs of potential mistakes that can be stated formally and reasoned about automatical...
