[Andrei Lapets] Accessible Formal Methods

3:00 PM Wednesday, April 17th, 2013

Towards Accessible Domain-Specific Integration and Deployment of Formal Tools and Techniques

Andrei Lapets

Postdoctoral Fellow
The Hariri Instititute

Abstract: Researchers in the programming languages and formal verification communities have produced a variety of formal analysis and verification tools and techniques. While there exist notable successes in using these tools to develop safe and secure software and hardware, they remain underutilized by large populations of users that may benefit from them. We adopt the following assumptions: (1) many new domain-specific languages (DSLs), tools, and techniques will inevitably continue to appear as a natural consequence of specialization; (2) the value of existing tools and techniques depends in part on how quickly and easily they can be integrated behind domain-specific interfaces and deployed; and (3) tools and techniques can be presented to users as parallel, complimentary, and interdependent abstract interpretations of a DSL along different dimensions (such as safety, cost, resources required, and so on).

Motivated by these assumptions, we present our work in assembling a supporting infrastructure (i.e., languages, modules, and libraries) for rapidly defining small DSLs and translations thereof to existing tools (e.g., Alloy, SPIN, Z3) and techniques (e.g., evaluation, type checking, congruence closure). The infrastructure also makes it possible to compile and deploy these DSLs, translators, and techniques in the form of cloud-based web applications with interfaces that run inside a standard browser.

We discuss and illustrate how this infrastructure can be used to help researchers, instructors, and students benefit from existing formal tools and techniques in applications such as classroom instruction of mathematics, modeling and design of safe distributed systems, and design of algorithms for quantum computers.

Bio: Andrei Lapets is a postdoctoral fellow and instructor in the Computer Science Dept., and an instructor in the Mathematics and Statistics Dept. at Boston University. He is also a consultant for the Quantum Information Processing Group at Raytheon BBN Technologies. His research interests include investigating ways to improve the accessibility of formal reasoning tools, and designing domain-specific high-level languages for application domains. In 2011, Andrei received a Ph.D. in Computer Science from Boston University, and he holds S.M. and A.B. degrees in Computer Science and Mathematics from Harvard University.