Automata and Computability using Jupyter and Formal Methods

Speaker:  Ganesh Lalitha Gopalakrishnan – Salt Lake City, UT, United States
Topic(s):  Society and the Computing Profession


Automata and computability form central theoretical pillars of computer science, and as such are included in almost all undergraduate curricula.  In the study of these topics, it is common practice to define machines, grammars and languages almost exclusively in mathematics.  Unfortunately, such definitions possess subtle nuances that can often be missed by most students.  Mathematical definitions are like code that has never been run (paraphrasing Knuth).  Providing feedback to students in small increments and without TA/grader delay is also a problem in the face of today's growing class sizes.

In a book written by this author entitled "Automata and Computability: A Programmer's Perspective" (2019), we take the approach of introducing this material accompanied by interactive Jupyter notebooks called "Jove". These notebooks allow the student to experiment with various constructions step by step in a read-eval-print loop.  They also employ Jupyter widgets that provide animations right within the notebooks.

More importantly, Jove also allows students to apply Boolean operations to verify that all the returned answers conform to reference specifications. When students make mistakes, they also get to experience entire classes of counterexamples in a single step, and are better able to learn from their own mistakes.  These steps are essentially what formal verification methods entail. Thus, the student gets to experience formal verification methods in an undergraduate class setting -- something that has been pointed out as being desirable at the undergraduate level.

Yet another benefit obtainable is by studying Jove's Python functions that are written largely using a subset of Python in a functional programming style.  In our codes, we employ recursion and also higher order functions such as map, reduce, fold, and filter. The importance of recursive programming and higher order functions is widely recognized; virtually all modern programming languages include these elements.

Last but not least, this approach incorporates many concepts that are seldom discussed in other similar courses – including derivative-style pattern matching, Binary Decision Diagrams, interactive experience with an efficient Post Correspondence Problem solver, a Boolean Satisfiabiity solver, and Lambda Calculus. All these ideas can be explored interactively within Jove.  Modernization of undergraduate syllabus by including such basic tenets of formal methods has long been raised by prominent researchers and educators as highly desirable.

This talk will be accompanied by a live presentation of how to use the book and Jove in a class setting. It will also provide feedback obtained from an external evaluator who used this book and software.

About this Lecture

Number of Slides:  60
Duration:  50 minutes
Languages Available:  English
Last Updated: 

Request this Lecture

To request this particular lecture, please complete this online form.

Request a Tour

To request a tour with this speaker, please complete this online form.

All requests will be sent to ACM headquarters for review.