关键词：大规模开放网络课程；MOOC；计算机科学
摘 要：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 Spring 2014, a graduate course was taught at UC Berkeley to explore the use of formal methods for a range of activities in online and large-scale education, including utomatic grading, synthesizing new problems, automatically solving problems, and creating and managing virtual laboratory environments. Students performed a range of projects exploring these topics for courses in computer science, electrical engineering, and other disciplines. This technical report includes the final reports on student projects along with a summary of some of the main lessons learned through in-class discussions.