The program analysis group focuses on automated verification using program analysis techniques to build reliable and secure programs with an emphasis on parallel, distributed, and concurrent systems software. PAG is currently exploring program analysis techniques for analyzing MPI programs, database applications, and web applications with a goal of making them more reliable by exploring scenarios often overlooked by programmers.