Can you convince me why your software works?

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

• Anvesh Komuravelli, Carnegie Mellon University
• Tuesday 17 March 2015, 09:00-10:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

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 http://research.microsoft.com. 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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.