Course Websites

Subject offerings of new and developing areas of knowledge in computer science intended to augment the existing curriculum. See Class Schedule or departmental course information for topics and prerequisites. Course Information: May be repeated in the same or separate terms if topics vary.

What will it take to build a world in which programmers of all skill levels can formally prove the absence of costly or dangerous bugs in software systems? This seminar will explore technologies for automating formal proofs about software systems in proof assistants like Coq, Lean, or Isabelle/HOL. Example topics include languages for proof automation, automated theorem proving for proof assistants, neural proof synthesis, and building usable automation. These topics will be explored through a combination of paper reading and collaborative exploration of code artifacts. Background in functional programming is expected; background in proof assistants is not needed. The website can be found at https://dependenttyp.es/classes/598fa2022.html. For up-to-date information about CS course restrictions, please see the following link: http://go.cs.illinois.edu/csregister