2018/11/16 by Bishoksan Kafle, Kafle, Bishoksan, Graeme Gange +8
Computer Science · Engineering · Mathematics · #Algorithm #Artificial intelligence #Combinatorics #Computer science #Construct (python library) #Dimension (graph theory) #Engineering #FOS: Computer and information sciences #Formal Methods in Verification #Inference #Logic in Computer Science (cs.LO) #Mathematics #Modularity (biology) #Partition (number theory) #Precondition #Programming language #Radiation Effects in Electronics #Set (abstract data type) #Software Testing and Debugging Techniques #Task (project management) #Theoretical computer science #cs.LO
paper · pdf · doi:10.48550/arxiv.1811.06771
19 pages, 8 figures
arxiv created 2018/11/16 · openalex publication_date 2018/11/16 · arxiv updated 2018/11/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Each iteration maintains over-approximations of the set of safe and unsafe initial states. Then we repeatedly use the current abstractions to partition the program's initial states into those known to be safe, known to be unsafe and unknown, and construct a revised program focusing on those initial states that are not yet known to be safe or unsafe. An experimental evaluation of the method on a set of software verification benchmarks shows that it can solve problems which are not solvable using previous methods.