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.
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.