Automated Tools for Assisting Formal Reasoning

SPRING 2012 RESEARCH INCUBATION AWARDEE

Andrei Lapets (Hariri Institute Postdoctoral Fellow)

Research communities in formal verification and in programming languages have developed many tools for formal reasoning and methods. These tools, however, have typically been difficult to use for students and researchers in other domains. This project focuses on developing and evaluating domain-specific environments that integrate multiple automated tools for assisting formal reasoning. For example, such tools could be used in the understanding and development of security protocols that require proofs about their security characteristics. Another application is in the math classroom, in which students can use a proof assistant to help them work through algebra proofs.

This work is funded by a Hariri Research Award made in June, 2012.