Robustness is an important aspect of software quality. One common way to improve robustness is to add preconditions to block in-puts that cause exceptional behavior. Ideally, programmers desire a both su?cient and necessary precondition. However, computing such precon-ditions is very challenging, especially for loop-related exceptions.
To address this challenge, we present a new approach implemented, in Pexum, to generate preconditions that are both su?cient and necessary. Pexum leverages three techniques to infer preconditions even in the pres-ence of input-dependent loops.