CS 477 - Formal Software Development Methods (Spring 2019)

CS 477 - Formal Software Development Methods (Spring 2019)

Madhusudan Parthasarathy (aka Madhu)

Wed and Fri 9:30am-10:45am, 1304 Siebel Center

Madhusudan Parthasarathy
Lecture Schedule
Homework Schedule
Papers, textbook chapters, tools
Project page
Piazza Website
Link: Primarily for grades

Scientific methods for engineering reliable software is a grand challenge in computer science, and of great need in our society that's growing more dependent on software systems.

This course is dedicated to studying formal techniques for building reliable software. The course will first teach the mathematical foundations of proving programs correct, logically, and how to reduce program verification to a mathematical theorem. Using this foundation, it will inspire contract based programming, a way of formally *specifying* properties of code and that facilitates modular reliable program development. The course will also cover a range of program verification and bug-finding techniqes that are based on formal mathematical techniques.

The course will be a mixture of theory and practice; it will involve learning about logics, proof systems, Hoare logic, program verification using theorem proving, decidable logics using SMT solvers, etc. as well as practical applications of these techniques in tools that enable program verification, proving simple properties using abstraction based techniques, symbolic testing techniques based on logic, and building programs using contracts.

We will use no textbook. All material will be available online.

Initial Logistics
WARNING: these pages are still tentative. Don't trust the details until the first few lectures are done. As soon as possible, you should get onto Piazza and Moodle, the two tools we will be using throughout the term. Instructions on how to sign up will appear soon here.

When you sign up for Piazza, ignore any warnings from the Piazza sign-up about requiring a U. Illinois email address: you should be able to register using any email address you like, including an anonymous email id.

Very little appears directly on this page. Routine announcements are posted on Piazza, Moodle, or the notes from each lecture. Check out the menu above for the Lectures page and information on other topics such as course policies, homeworks, and exams.