|
Computer Science Seminar Date: Monday, 28 October 2024 Time: 12:00 - 01:00 PM Venue: Seminar Hall Weakest Precondition Inference for Linear Array Programs Sumanth Parbhu TCS Research. 28-10-24 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 specified postcondition. The weakest precondition refers to the largest such set of initial states. Such preconditions are useful in various practical applications related to software development, verification, and testing. Hence, its automatic inference is an important problem that has received considerable attention. However, existing techniques find it challenging to handle programs with arrays. In this talk, I will present our technique for finding quantified weakest preconditions for programs with arrays. Our approach is effective for a class of programs called linear array programs. While we prove that the computation of the weakest precondition for linear array programs is undecidable, such programs frequently appear in practice. Therefore, we propose an approach in the Infer-Check-Weaken framework. This approach 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. We experimentally show that our approach outperforms the state of the art on a set of publicly available benchmarks. 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). Speaker bio: Sumanth Prabhu works as a scientist in the Foundations of Computing group at TCS Research. He did his Masters from CMI and 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.
|
