Seminars & Workshops

Completeness of Pointer Program Verification by Separation Logic

Speaker:	Makoto Tatsuta , National Institute of Informatics
When:	2010-03-15 14:00
Place:	Room 308, Bldg 302, SNU

Abstract

Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem as well as the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion. This paper also introduces the predicate that represents the next new cell, and proves the completeness and the soundness of the extended system under deterministic semantics. This is a joint work with Wei-Ngan Chin and Mahmudul Faisal Al Ameen.

Short bio

Bachelors in Law in 1983 and Science in 1985, Master's in Science in 1987, and PhD in 1993 all in University of Tokyo. An assistant professor and an associate professor at Tohoku University from 1989 to 1996. An associate professor at Kyoto University from 1996 to 2001. A professor at National Institute of Informatics since 2001. Interested in theoretical computer science and mathematical logic, in particular, type theory and constructive logic.