BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Can you convince me why your software works? - Anvesh Komuravelli\
 , Carnegie Mellon University
DTSTART:20150317T090000Z
DTEND:20150317T100000Z
UID:TALK58445@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The rise of practical solvers for satisfiability checking (bot
 h propositional and first-order logics) has revolutionized the field of au
 tomatic program verification.  However\, present day algorithms make an in
 efficient use of these solvers by creating monolithic SAT instances for th
 e entire program that can\ngrow exponentially in size. I will first descri
 be an efficient "compositional" SAT-based approach for automatic verificat
 ion that exploits the modularity of the program under consideration.  This
  results in significant improvements over the state-of-the-art\, both in t
 heory and in practice. While SAT solvers can be used to explore bounded su
 bsets of the reachable state space\, program\nverification is undecidable 
 in general. To this end\, I will describe another compositional SAT-based 
 algorithm that improves practical convergence for an automatic inference o
 f formal correctness proofs. While correctness is an important aspect of e
 ffective software development\, there are several other issues\, e.g.  pro
 gram understandability\, to be concerned about. I will conclude with descr
 ibing some exciting future research directions\, both for ensuring correct
 ness and beyond.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR