Formal Methods for the Informal Engineer (FMIE) is a workshop aimed at highlighting recent successes in the development of verified software. On the first two days, to accommodate an audience consisting of many interested non-experts, we will have hands-on tutorials with two different verification technologies, the Coq and Z3 theorem provers. This will provide the audience with exposure to basic concepts of verification. The final day will feature four speakers presenting on General Topics, Verified Software Components, Distributed Systems, and Robust Machine Learning.

The vision to host FMIE at the Broad Institute originated in conversations about economic incentives, exponential growth of multi-modal data sources, and challenging biomedical problems which have resulted in the life sciences emerging as both key consumers and producers of software and AI technologies. The next 5 -10 years will be a critical growth phase for this process and provide an opportunity to shape the software engineering culture from the ground up. Safety and security, realized through both informal and formal methods, are central to this goal.

Ultimately, our aim is to further the development of reliable software systems by creating a venue for collecting the success stories of formal methods, exploring applications to real-world software development, and connecting researchers to aspiring users. Although FMIE was initially conceived with a view towards ongoing developments in the life sciences, the topics and speakers we have selected are domain-agnostic. We welcome participants from any arena in which the development of robust software systems would be impactful.

Program Commitee

Gopal Sarma, Broad Institute of MIT and Harvard
Jimmy Koppel, MIT CSAIL
Ramana Kumar, DeepMind
Eric Drexler, James Martin School at Oxford University
Patrick Schultz, Broad Institute of MIT and Harvard
Gregory Malecha, BedRock Systems