计算机学院系列报告会之——Dr. Christian Urban

发布时间:2010-12-31浏览次数:75

报告题目:Verifying A Regular Expression Matcher and Formal Language Theory

 

报告人:Dr. Christian Urban

时 间:4月15日下午3:00~4:00

地 点:计算机学院六楼学术报告厅

 

报告摘要:
Verifying formally the correctness of an algorithm is still fiendishly hard. One way of making such verifications easier is to implement the algorithm directly inside a theorem prover. In the talk I will show how to do this with a simple regular expression matcher. This example will also show that often an algorithm needs to be re-formulated in order to better suit the reasoning in a theorem prover. For example, regular expression matching is normally implemented with finite automata. Unfortunately, automata are a hassle for formalizations in theorem provers, in our case the theorem prover Isabelle/HOL. The reason is that automata need to be represented as graphs or matrices, neither of which can be easily defined as algebraic datatype. In contrast, regular expressions can be defined easily as datatype and a corresponding reasoning infrastructure comes for free. I will show in the second part of the talk that a central result from formal language theory, the Myhill-Nerode theorem, can be recreated using only regular expressions.

This is joint work with Chunhan Wu and Xingyuan Zhang from the PLA University of Science and Technology in Nanjing.

 

报告人介绍:

Christian Urban is an Emmy Noether Fellow at the Technical University of Munich (Germany). He received his Ph.D. in 2000 from the University of Cambridge (UK). After his Ph.D., he was awarded a research fellowship at Corpus Christi College in Cambridge. In 2004 he moved back to Germany with the help of a fellowship from the Alexander-von-Humboldt Foundation.

His current research interests include theorem provers, type systems, compilers, formal languages, and semantics of programming languages.

 

举办单位:欧亿6蓝狮在线

[CS-2011-006]