"Model Finding: Applications, Completeness, and Usability"
Tim Nelson, Brown University
Thursday, February 22, 2018 at 4:00 P.M.
Room 316 (CIT 3rd Floor)
Model-finding tools accept a set of constraints and produce concrete logical structures (i.e., models) that satisfy the input. They can verify whether desired properties hold about a system and can even help explore system behavior in the absence of properties. Applications abound in fields such as software engineering, networking, and security. My own work has used model finders to analyze and explore access-control policies, firewall configurations, software-defined network programs, and more.
Depending on their underlying logic, model finders can be incomplete: their search for models may produce a false negative. Incompleteness is unavoidable for (e.g.) general first-order logic model finders. Fortunately, for many domains, the full expressive power of the logic is unnecessary and completeness can be reclaimed. I will discuss a decidable fragment of order-sorted first-order logic, OS-EPL, that encompasses numerous application domains and enables complete analysis for multiple tools.
It is not enough for model finders to be mathematically rigorous or intuitively appealing. They, and tools built atop them, are ultimately intended to be used. My work therefore involves user studies to evaluate their effectiveness. The results of these studies suggest that otherwise intuitive choices (for instance, in which models to present) may hinder users in some circumstances.
Tim Nelson is a Senior Research Associate at Brown University. He received his PhD in Computer Science from Worcester Polytechnic Institute. His research lies mainly in user-facing formal methods, particularly in applications such as networking and configuration management. He is the designer and instructor of Logic for Systems, a popular introductory formal methods course at Brown.
Host: Professor Philip Klein