University of Cambridge > > Microsoft Research Cambridge, public talks > Can you convince me why your software works?

Can you convince me why your software works?

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity