CSAIL Event Calendar

PL Seminar: Towards an Infrastructure for Accessible Integrated Formal Reasoning Environments

Abstract: Computer science researchers in the programming languages and formal verification communities have produced a variety of automated tools and techniques that can assist end-users engaging in high-level formal reasoning tasks (e.g., algorithms and systems that implement model checking, state space search, type checking, logical inference and verification, non-interference checking, and so on). In this context, we consider the following end-user: a domain expert (e.g., a protocol designer, a researcher, a student) who is familiar with rigorous mathematics and is interested in using some collection of these tools to automatically analyze formal constructs within his or her domain. However, this end-user may be unaware of what tools are available, and is unwilling to spend any time installing tools, learning to use individual tools, translating the problem of interest to a form that fits each of the tools or techniques, or interpreting the various outputs within the context of the domain. We pose the following general problem: for a chosen domain and collection of component tools and techniques, how can we coordinate and support the task of defining, implementing, and delivering a formal reasoning environment that seamlessly integrates the various components and is sufficiently accessible (both logistically and semantically) to accommodate such an end-user.

We present our ongoing efforts to address this problem by identifying some features an infrastructure that aims to support this task might possess and some conventions it might follow (there could eventually be many such infrastructures assembled by different communities). Some of these features are illustrated with the help of a prototype infrastructure that includes a language, conventions, compilers, and other elements that support the integration and delivery of the capabilities of several components within a ready-to-use web application that runs entirely within a standard web browser. We describe some of the interesting programming challenges that arise and the opportunities they present to designers of future high-level programming languages. If time permits, we review current efforts to use constructed environments in classroom instruction and for modelling secure protocols.


Speaker bio: Andrei Lapets is a postdoctoral fellow and lecturer at the Hariri Institute at Boston University. His research interests include investigating ways to improve the accessibility of formal reasoning tools, and designing domain-specific high-level languages for application domains such as constrained flow networks, service-level agreements for cloud computing resources, and quantum computing. In 2011, Andrei received a Ph.D. in Computer Science from Boston University, and he also holds S.M. and A.B. degrees in Computer Science and Mathematics from Harvard University.

See other events happening in June 2012