Dr.Christian Urban Visited Joint Research Center

On April 25, 2011 at the invitation of USTC-Yale joint research center for confidence software, Dr. Christian Urban from German Technical University of Munich paid a visit to USTC Suzhou Institute. Dr. Christian received his PhD degree from Cambridge University in 2000 and after that he has been engaged in research work related to theorem proof in Cambridge University, Princeton University and Technical University of Munich. In recent years, he mainly focuses on theoretical fields like auto theorem proof , program language,etc.
Nowadays, Dr. Christian Urban is one of the key developers of the famous theorem proof device named Isabelle. With the group’s work they aim to provide all proving technologies necessary for reasoning conveniently about programming languages and compilers. During his visit, Dr. Christian Urban gave a brilliant introduction about Isabelle to our teachers and students. He clearly illustrated every aspect of Isabelle, deeply analyzed its differences from other proof assistants, and expertly answered many questions raised by our students. Besides, in high spirits he demonstrated the usage of Isabelle and its features. The discussion lasted for all the afternoon, where Dr. Christian Urban and our teachers and students made an in-depth exploration to research work implemented by each other, and finally reached consensus on long-term exchanges and cooperation.

 Dr.Christian Urban is discussing with Pro.zhong shao about the future cooperation plan.

Dr.Christian Urban is showing how to use isabelle.

Dr.Christian Urban is talking with the students of the center.