Can you convince me why your software works?

  • Anvesh Komuravelli, Carnegie Mellon University; Josh Berdine, Microsoft

The rise of practical solvers for satisfiability checking (both propositional and first-order logics) has revolutionized the field of automatic program verification. However, present day algorithms make an inefficient use of these solvers by creating monolithic SAT instances for the entire program that can grow exponentially in size. I will first describe an efficient “compositional” SAT-based approach for automatic verification that exploits the modularity of the program under consideration. This results in significant improvements over the state-of-the-art, both in theory and in practice. While SAT solvers can be used to explore bounded subsets of the reachable state space, program verification is undecidable in general. To this end, I will describe another compositional SAT-based algorithm that improves practical convergence for an automatic inference of formal correctness proofs. While correctness is an important aspect of effective software development, there are several other issues, e.g. program understandability, to be concerned about. I will conclude with describing some exciting future research directions, both for ensuring correctness and beyond.

Speaker Details

Anvesh Komuravelli is a PhD student in the Computer Science Department at Carnegie Mellon University, working with Prof. Edmund M. Clarke. His research interests are in scientific methods for building computer systems that are correct, efficient, and maintainable. As part of his PhD, he worked on new and efficient automatic verification techniques for safety of programs using state-of-the-art satisfiability solvers. He published in top venues such as CAV and LICS. He has a Bachelors degree in Computer Science from the Indian Institute of Technology Kharagpur. Outside of work, he makes time for learning vocal music and piano, and giving stage performances.

Watch Next