Elsa Gunter

Ph.D. University of Wisconsin-Madison, 1987

Research Statement

The focus of my research has been and continues to be on theorem proving with an automated assistant, and its application to reasoning about protocols, programs and programming language semantics. Theorem provers capable of supporting general mathematical reasoning offer the greatest flexibility for developing programming language semantics and for proving properties of programs. However, to be truly useful for such applications, much specialized infrastructure must be available as well. For the immediate future, I plan to apply automated theorem proving to reasoning about domain specific languages, particularly ones for networking and security. To support such reasoning, I am working on better integration of HOL90, and possibly related theorem provers, with model checkers and other fully automatic tools for theorem proving.