 |
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, |
Course
Web-site for Programming Languages (CS 421 Fall 2009)
Course Web-site for Programming Languages Design(CS 422 Spring 2009)
Course Web-site for
Topics in Automated Deuction (CS 5761 Spring 2010)
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.