Transformation-Enabled Precondition Inference
Bishoksan Kafle, Graeme Gange, Peter J. Stuckey, Peter Schachte,, Harald Sondergaard

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
