Natural Proofs for Computer-Aided Programming ALS 4001 Mon, 04/04/2016 - 9:00am
Xiaokang Qiu Postdoctoral Associate, MIT Computer Science and Artificial Intelligence Laboratory Abstract: 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. Bio: URL: http://eecs.oregonstate.edu/colloquium/natural-proofs-computer-aided-programming _______________________________________________ Colloquium mailing list [email protected] https://secure.engr.oregonstate.edu/mailman/listinfo/colloquium
