Exploring Software Assistants for Formal Methods

SPRING 2011 RESEARCH INCUBATION AWARDEE 

Assaf Kfoury (Computer Science, College of Arts & Sciences)

As computing technology continues developing, new techniques, infrastructures, tools, and interfaces are advancing dramatically: the collaborative or “crowd-sourced” assembly of Wikipedia, IBM’s Watson question-answering system, ubiquitous palm-sized computing devices with intuitive interfaces, and so on. The user interface design (UID), human-computer interaction (HCI), and artificial intelligence (AI) communities have studied and developed methodologies and techniques (in which accessibility and usability play a central role) for building, designing, and empirically evaluating systems and tools that are to be employed by human users. To the best of our knowledge, these modern methodologies have not been employed deliberately and extensively in the design of modern formal reasoning assistance tools. This project aims to leverage contributions of the UID, HCI, and AI communities to design and test new approaches to building interfaces for formal reasoning, modelling, search, and verification tools.

This work was funded by a Hariri Research Award made in June, 2011.