Hariri Institute Distinguished Lecture - Andrei Lapets
- 3:00 pm on Wednesday, April 17, 2013
- 5:00 pm on Wednesday, April 17, 2013
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.