主 题: Information Sceicences Seminar—— Auto2 prover in Isabelle and its application to program verification
报告人: Dr. Bohua Zhan (Technical University of Munich, Germany)
时 间: 2018-04-26 10:00-12:00
地 点: Room 1303, Sciences Building No. 1
Abstract: Interactive theorem proving is concerned with building formal proofs on a computer with human guidance. In this field, a human communicates the main ideas of the proof in the form of "proof scripts". The computer, following the proof script, produces and checks a fully-detailed proof in some logical foundation. Proof automation, used to automatically construct large parts of the proof, is an important part of an interactive prover. The stronger the proof automation is, the simpler are the proof scripts that humans are required to enter.
In this talk, I will give an overview of the field of interactive theorem proving. I will then discuss my own work on a new proof automation tool called auto2, implemented in the interactive theorem prover Isabelle. Finally, I will describe some applications of auto2, focusing on verification of imperative programs.
Speaker Bio: Dr. Bohua Zhan is currently a postdoctoral fellow at Technical University of Munich. He received his Bachelor's degree from Massachusetts Institute of Technology in 2010 and PhD in mathematics from Princeton University in 2014. He is then a postdoctoral fellow at MIT from 2014 to 2017. While in graduate school, he worked on low dimensional topology. More recently he is working on automation in interactive theorem proving, and its application to formalization of mathematics as well as program verification.
