题目：Correctness of Substring Pattern-Preprocessing in Boyer-Moore’s Pattern Matching Algorithm.
主讲人：Frank Stomp
时间：2005年6月21日下午2：00
地点：曹光彪西楼201教室
Abstract: One of the fastest known pattern matching algorithms is the one developed by Boyer and Moore. It utilizes two preprocessing algorithms: One of these is based on characters; the other one is based on substrings. After a brief introduction to the area of Formal Software Verification, I will focus on correctness of the latter preprocessing algorithm. It will be shown that that most published versions of the substring preprocessing algorithm contain a (minor) error. The error has been corrected and a sketch of correctness of the corrected version will be presented.
Since the entire proof is complicated, the correctness proof has been mechanically checked using the PVS theorem prover. If time admits, I will also discuss part of the mechanical proof. (The mechanization of the correctness proof has been carried out in collaboration with Milos Besta.)
Frank Stomp’s research is in the area of Formal Software Verification.
He received a B.S. and an M.S. from the University in Utrecht (The Netherlands), and a Ph.D. in Computer Science from Eindhoven University of Technology (The Netherlands). He is currently an Associate Professor in the Department of Computer Science of Wayne State University (USA).
计算机学院（软件学院）
2005年6月20日
主讲人：Frank Stomp
时间：2005年6月21日下午2：00
地点：曹光彪西楼201教室
Abstract: One of the fastest known pattern matching algorithms is the one developed by Boyer and Moore. It utilizes two preprocessing algorithms: One of these is based on characters; the other one is based on substrings. After a brief introduction to the area of Formal Software Verification, I will focus on correctness of the latter preprocessing algorithm. It will be shown that that most published versions of the substring preprocessing algorithm contain a (minor) error. The error has been corrected and a sketch of correctness of the corrected version will be presented.
Since the entire proof is complicated, the correctness proof has been mechanically checked using the PVS theorem prover. If time admits, I will also discuss part of the mechanical proof. (The mechanization of the correctness proof has been carried out in collaboration with Milos Besta.)
Frank Stomp’s research is in the area of Formal Software Verification.
He received a B.S. and an M.S. from the University in Utrecht (The Netherlands), and a Ph.D. in Computer Science from Eindhoven University of Technology (The Netherlands). He is currently an Associate Professor in the Department of Computer Science of Wayne State University (USA).
计算机学院（软件学院）
2005年6月20日
