Tapping into Formal Methods for Pedagogical Adrenaline Rush: Possible?

Ganesh Gopalakrishnan
Professor, Computer Science Department, University of Utah

Stevenson Hall 1300
12:00 PM - 12:50 PM

Formal methods have traditionally evolved around the core concepts of specifying systems and matching system behaviors against the specifications. How successfully can existing Formal Methods be tapped into for rejuvenating today's undergraduate curricula? I will introduce the pivotal role played by Formal Methods in safeguarding today's software and hardware, and then present a few attempts I have made in bringing it down into the undergraduate curriculum. My illustrations span the classical Automata Theory, Boolean Logic, Concurrency and Automated Theorem-Proving. 

I will go through topics such as Automata Theory, Binary Decision Diagrams, and Satisfiability-Modulo Theories to illustrate my point through examples that can be dropped into curricula. These examples cover situations from games through solving the scheduling of concurrent programs.

It is my growing belief that the thrill of seeing hard problems fall victim to the power of automated tools can give the adrenaline rush that makes a topic fun to learn. Treating these topics pedantically is acceptable for mathematical maturity; but must ideally also be complemented with illustrations that make the students see the research and industrial horizons opened up by formal methods.