EECS 294-98: Formal Methods for Engineering Education

Spring 2014

General Information

Instructor: Sanjit A. Seshia (office: Cory 566)
Class Hours and Location:
Monday & Wednesday, 2:30 - 4 pm, in 293 Cory
Office Hours:
Monday & Wednesday, 1:30 - 2:30 in 566 Cory
Credits: 3 units
Check the bSpace site for this course regularly.

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: http://www.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-170.html.

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.

Project: 70%
The course project is the most important component of this class. It can be a theoretical and/or experimental investigation related to topics covered in class. A list of project topics will be announced in the first three weeks of the semester. You are also encouraged to pick topics of your own, after consulting with the instructor. It is expected that students team up in groups of 2 or 3 for their project. Projects will culminate in a final paper, presentation, and possibly a demo.
Paper Discussions: 20%
Students will have to present at least one paper listed on the schedule and lead discussion on the paper.
Class Participation: 10%
All students must read assigned papers and participate in discussions.

Projects

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.

Jan 27: Introduction to the course (PDF).
Read this paper by Lee and Messerschmitt: A Highest Education in the Year 2049.
Jan 29: Problem Specification: Intro to propositional logic, first-order logic, automata models. (done on the blackboard)
Feb 3: Problem Specification: Temporal logic overview: LTL, MTL, STL etc. (PDF on LTL, PDF on STL)
Feb 5: Project discussion (Slides in PDF)
Feb 10: Problem Solving: Formal Verification overview I - Model checking, SPIN demo (done on the blackboard, link to SPIN model)
Feb 12: Problem Solving: Verification with Satisfiability (SAT/SMT) Solving overview, UCLID demo (done on the blackboard, link to UCLID model)
Feb 17: President's Day holiday
Feb 19: Bridging Natural Language and Formal Languages (guest lecture by S. Ghosh and W. Li, SRI International)
Feb 24: Problem Solving: Formal Verification overview II (run-time/simulation-based verification, synthesizing test cases with focus on hybrid systems models) PDF slides)
Feb 26: Project proposal presentations.
Mar 3: Syntax-Guided Synthesis overview: PDF of paper, PDF of slides
Mar 5: Paper discussion: Auto-grading Python programs by Singh et al.
Mar 10: No lecture, attend as much of the ExCAPE annual meeting as you can. See especially the Tuesday morning session on online education.
Mar 12: Guest lecture by S. Gulwani (MSR) on Automatically Generating Problems and Solutions for Natural Deduction by Ahmed et al.
Mar 17: Paper discussion: Automata Tutor by Alur et al.
Mar 19: Project Update Presentations
Mar 24,26: Spring Break, no classes
Mar 31: Guest lecture by Jeff Jensen (NI) on a Virtual Laboratory environment: modeling, auto-grading and feedback-generation issues. Here's a related paper: Virtualizing Cyber-Physical Systems: Bringing CPS to Online Education.
Apr 2: Paper discussion: Automatic problem generation by Singh et al., and Automating Exercise Generation: A Step towards Meeting the MOOC Challenge for Embedded Systems by Sadigh et al.
Apr 7, 9: Project update presentations: 10 minutes presentation with 5 minutes for questions and discussion per group.
Apr 14: Guest lecture by Derrick Coetzee on designing user studies, evaluating software for MOOCs, etc.
- Related paper: Kohavi et al., Controlled experiments on the web: survey and practical guide.. Most relevant sections are 1, 3, 5.
- Relevant info on Berkeley's IRB process: Student Investigators Guide, Exempt Research Categories, Expedited Review Procedure.
Apr 16: No class Sanjit away at a funding review. Work on your projects!
Apr 21: Paper discussion: Crowd-scale Interactive Formal Reasoning and Analytics by Fast et al.
Apr 23: 5-min Project updates.
Apr 28: Discussing papers from non-formal methods literature: Syntactic and Functional Variability of a Million Code Submissions in a Machine Learning MOOC and Codewebs: Scalable Homework Search for Massive Open Online Programming Courses .
Apr 30: Summary of main ideas learned. Discussion of future work.
May 7: Project presentations/poster session

Tools

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.