 |
Elsa L Gunter
Research Associate Professor, Department of
Computer Science, University of Illinois,
Urbana - Champaign,
|
Elsa L GunterResearch Associate Professor, Department of
Computer Science, University of Illinois,
Urbana - Champaign, |
Research Interests: Software engineering; formal methods; design and use of automated and interactive theorem provers; mathematical semantics of programming languages; proof theory and type theory; order theory.
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.