EECS 294-98: Formal Methods for Engineering Education

Spring 2014

Short-cuts: [   Description   |   Prerequisites   |   Books/Reading   |   Grading   |   Projects   |   Schedule   |   Tools   ]

General Information

Technical Report: We have published the research-oriented final course project reports along with a summary of the concepts studied and lessons learned in the Spring 2014 course here:

Course Description

The advent of massive open online courses (MOOCs) has placed a renewed focus on the development and use of computational aids for teaching and learning. In this course, we will explore the use of formal methods for a range of activities related to online education, including automatic grading, synthesizing new problems, automatically solving problems, and creating and managing virtual laboratory environments. The material covered will be broadly relevant to courses in Electrical Engineering and Computer Science, although some concepts may also be applicable to other science and engineering disciplines.

The course will cover foundational topics in formal methods, such as the use of mathematical logic and automata theory for formal modeling, and algorithmic techniques for verification and synthesis such as model checking, Boolean satisfiability (SAT) solving, and satisfiability modulo theories (SMT) solving. However, unlike EECS 219C, which teaches you how to develop new algorithms for formal verification or synthesis, this course will teach you how to effectively use and adapt formal methods for problems in engineering education. Relevant topics related to user interface and evaluation studies will also be covered via guest lectures.

Following the introductory lectures on foundational topics, students will read and lead discussions on papers in the area, and propose and complete a final project. A list of suggested projects will be provided for developing technologies for an online version of EECS 149 (Introduction to Embedded Systems) and for similar courses that have a significant laboratory component. Students are also encouraged to propose their own project topics aligned with the course goals.


Basic mathematical maturity and familiarity with fundamental algorithms and data structures at an undergraduate level. No background in embedded systems is required. If you are unsure whether you have sufficient background for the course, please meet the instructor.

Reference Books

There is no required textbook for this course. Readings will be listed on the schedule below or posted on bSpace; you should come prepared to take notes. The following books may be used in selected parts of the course (copies will be on reserve at the Engineering library):
  1. Authors: Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled
    Title: Model Checking
    Publisher: MIT Press
    Year: January 2000
  2. Authors: Michael Huth and Mark Ryan
    Title: Logic in Computer Science: Modelling and Reasoning about Systems
    Publisher: Cambridge Univ. Press
    Year: June 2004 (2nd edition)
  3. Authors: Edward A. Lee and Sanjit A. Seshia
    Title: Introduction to Embedded Systems: A Cyber-Physical Systems Approach
    Year: 2011
  4. Author: Gerard Holzmann
    Title: The SPIN Model Checker: Primer and Reference Manual
    Publisher: Addison-Wesley
    Year: September 2003


All projects will be auto-graded based on technology developed in the class.
Just kidding!! See below for details on how grading will work:


Project topics discussed in class; see the schedule below.

Course Topics and Schedule (subject to change)

The tentative course schedule is given below. Slides, if any, will be posted alongside; readings will be posted on bSpace.
Note that classes will begin January 27.


Here is an incomplete list of tools that could be useful in your projects.

Finite-State Model checking tools:

SMT solvers and SMT-based verification tools: Timed / Hybrid systems verification / synthesis tools: Links to more tools will be added here as needed.
Copyright 2013-14 Sanjit A. Seshia
Last modified: Mon Apr 7 14:04:07 PDT 2014