ABSTRACT:

We consider sequential programs with multiple loops, where the iteration count of each loop depends on a set of parameters. Examples of such programs include those that manipulate data structures of parametric sizes, or iteratively compute scalar functions of the parameters. Properties of such programs can often be expressed as parameterized Hoare triples, where the pre- and post-conditions depend on the parameters on which the loop iteration bounds depend. We present a technique called generalized full-program induction for reasoning about a large class of such programs, while bypassing the need for computing loop invariants for each loop. This approach effectively shifts the granularity of inductive reasoning from individual loops to the entire program comprised of possibly many loops. We have implemented this technique in two tools called Vajra and Diffy. Our experiments show significant performance improvements using full-program induction vis-a-vis other state-of-the-art techniques. Full-program induction is a key back-end engine in the tool VeriAbs that has been the winner in the ReachSafety category of SVCOMP (software verification competition) for the last few years.

 BIO:

Supratik Chakraborty is Bajaj Group Chair Professor in the Department of Computer Science and Engineering at IIT Bombay. His research interests include constrained sampling and counting, automated synthesis, formal verification, automata theory and logic. He is particularly interested in the development of scalable algorithmic techniques with strong guarantees for reasoning about different computational models. Supratik is a Distinguished Member of ACM and an elected Fellow of Indian National Academy of Engineering.

Hosted by Professor George Varghese