Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of safe and unsafe initial states; which are used to partition the program's initial states into those known to be safe, known to be unsafe and unknown. We then construct revised programs with those unknown initial states and iterate the procedure until the approximations are disjoint or some termination criteria are met. An experimental evaluation of the method on a set of software verification benchmarks shows that it can infer precise preconditions (sometimes optimal) that are not possible using previous methods.

翻译：有条件的推断是程序分析和核查中重要应用的非三重性问题。 我们提出了一个新颖的迭代方法,用于自动得出程序安全和不安全的先决条件。 每套迭代方法都维持对一组安全和不安全初始状态的过份赞同; 用于将程序初始状态划分为已知安全、 已知不安全和未知状态。 然后我们与这些未知的初始状态建立订正程序,并在近似脱节或达到某些终止标准之前循环程序。 对一套软件核查基准上的方法进行的实验性评估表明,它可以推断出使用先前方法不可能达到的准确先决条件( 有时是最佳的)。