Collaborative Research: FMitF:Track III: A Taste of Formal Methods for Different STEM Communities and Courses

Formal methods in computer science aim to increase reliability and robustness of software and hardware designs. Unfortunately, formal methods are typically only accessible to specialized professionals. One of the reasons for this limited accessibility is the lack of exposure to formal methods in undergraduate education, even for computer science majors. Even though formal methods are used in practice to analyze the correctness of large-scale software and hardware systems, they can also be applied to algorithms and other mathematical constructs at a smaller scale. The project's novelties are developing and disseminating self-contained interactive exercises, using a web-based programming environment, to solve small-scale problems using formal methods. The project's impacts are that these small-scale problems give a taste of formal methods to different STEM communities, namely: three institutions (a research institution, a liberal-arts college, and a community college), several computing and engineering majors (computer science, bioinformatics, computer engineering, chemical engineering, and more), and several topics and levels (introductory programming, engineering design, digital system design, databases, artificial intelligence, and more). The project's impacts go beyond the investigators' institutions: The self-contained interactive exercises can be used as-is, with no work required from the instructor and no additional time needed in the course schedule since they are designed to cover standard course topics, to give a taste of formal methods to all. Formal methods are currently not part of the standard computer science undergraduate curriculum. Thus instruction using formal methods, especially outside of computer science programs and outside of research institutions, is very limited. Instructors may lack the proper experience or background to teach formal methods. Instructors may not have had the appropriate exposure, and for STEM instructors outside computer science (e.g., mechanical engineering), formal methods may be far away from their fields. Additionally, there is a lack of space in the often tightly structured undergraduate computing and engineering curricula. The project's working hypothesis is that formal methods exposure can be significantly improved by developing self-contained Jupyter notebooks (using satisfiability modulo theories solvers accessed via Python) that focus on small-scale problems. These notebooks can be used as-is, with no work required from the instructor and no additional time needed in the course schedule since they are designed to cover standard course topics. For instance, modules studying the verification of the molecular structure of a chemical compound, the links in a protein-protein interaction biological network, or the tuples retrieved by a SQL query over a relational database. The project aims to impact a wide range of students and majors. This includes computer science students at the Rochester Institute of Technology (RIT, a research institution) and the College of the Holy Cross (a liberal arts college), as well as at Monroe Community College, which has a formal transfer pathway with RIT. In addition to introducing formal methods to computer science students, the project will also introduce formal methods to several engineering programs. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.