Software Foundations

Software Foundations will be a project-based course focusing on the challenges and techniques involved in proving non-trivial properties about real-world systems. We will base our exploration around formal development in a proof environment. Roughly half of the course will be a guided tutorial of proof techniques using one or more theorem provers; in the remainder, students will apply this knowledge to existing systems. No prior experience with theorem provers or proof assistants is necessary, but familiarity with and aptitude for functional programming will be a huge bonus. Prerequisite: CSCI 1730 or equivalent; mathematical maturity.