Transformation-Enabled Precondition Inference

TL;DR

This paper introduces an iterative, transformation-based method for automatic precondition inference in program analysis, effectively distinguishing safe and unsafe initial states to improve verification precision.

Contribution

It presents a novel iterative approach that refines preconditions by partitioning initial states and constructing revised programs, achieving more precise results than previous methods.

Findings

Can infer precise, sometimes optimal, preconditions

Effective on software verification benchmarks

Outperforms prior precondition inference techniques

Abstract

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.