Languages

Dr. XiaoKang Qiu Visited USTC-Yale joint research center

On April 3, 2015, Dr.XiaoKang Qiu came to USTC-Yale joint research center and paid a two-day visit. XiaoKang Qiu got his PhD under the supervision of  Madhusudan Parthasarathy in 2013 at the  University of Illinois at Urbana-Champaign,  and he is currently employed as a post doc at MIT. His research interests span a range of areas in Programming Languages and Software Engineering, with focus on theories, algorithms and tools of Programming Systems, including program logics, decision procedures, automated deduction, program verification, and program synthesis. During that time, Dr. XiaoKang Qui gave us a talk about Natural Proofs for Computer-Aided Programming. 
 
The abstract of the talk is shown below:
 
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.