Computer software has revolutionized our daily lives, but software developers’ lives have not advanced commensurately. Programming remains an error-prone, human process, leading to defective programs that pose a severe threat to our society. I aim to help people build reliable software more easily and more productively by exploiting their own machines’ computing power. In this talk, I will present Natural Proofs, a radically new proof methodology that algorithmically proves sophisticated properties using a set of simple but practically useful proof tactics. Natural proofs can be deployed in various programming tools, such as verifiers that prove correctness of annotated programs and synthesizers that generate implementations from high-level specifications. I will describe how natural proofs can enhance the automaticity of these tools on building a wide variety of reliable heap-manipulating programs from open-source libraries and OS kernels. The natural proof-based verification and synthesis techniques hold promise of leading to the next-generation computer-aided programming systems, which alleviate programmers’ burden from all aspects, including coding, writing contracts, strengthening specifications, and providing proof hints.
Xiaokang Qiu is a postdoctoral associate in the MIT Computer Science and Artificial Intelligence Laboratory. He received his Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign in 2013. Dr. Qiu is interested in software verification and synthesis, with a particular emphasis on heap-manipulating programs. His research focuses on program logics, decision procedures, automated verification, and syntax-guided synthesis.