Title: Weakest Precondition Inference for Linear Array Programs

Speaker: Sumanth Prabhu    (bio) (bio)

Sumanth Prabhu works as a scientist in the Foundations of Computing group at TCS Research. He did his Ph.D. from the Indian Institute of Science, Bangalore, where he was advised by Deepak D'Souza. His current research focuses on formal verification and automated synthesis using constrained horn clauses.

When: Tuesday, 07 May 2024 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
The problem of precondition inference is to find a set of initial states from which all terminating executions of a given program reach states that satisfy a given postcondition. The weakest precondition refers to the largest such set of initial states. The weakest precondition is helpful in many practical problems around software development, verification, and testing. Hence, its automatic inference is an important problem and has received considerable attention. However, existing techniques find it challenging to handle programs with arrays.

In this talk, I will present our technique to find quantified weakest preconditions for programs with arrays. Our technique is effective on a class of programs called linear array programs. We prove that linear array programs' weakest precondition computation is undecidable. Nevertheless, such programs often appear in practice. Hence, many array works target them but for verification, not precondition inference. We propose a precondition inference technique in the Infer-Check-Weaken framework. It first infers a precondition along with adequate inductive invariants. A maximality check follows to see whether the precondition is the weakest. If not, the precondition is weakened. In this framework, we present novel methods for each module. We experimentally show that our technique is significantly better than the state-of-the-art over a set of existing linear array programs.

This talk is based on our two papers from ESOP 2024 and TACAS 2024. The work is done in collaboration with Deepak D'Souza (Indian Institute of Science), Grigory Fedyukovich (Florida State University), Supratik Chakraborty (IIT Bombay), and R Venkatesh (TCS Research).