Can you convince me why your software works?

Опубликовано 22 июня 2016, 2:55

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.