COMP 7730/7736

Formal Methods for Software Engineering

Instructor

Contact information: 
 
name: Richard Chapman 
email: chapman@eng.auburn.edu
phone: 844-6314
office: Dunstan 108

Goals and Objectives

After successfully completin this class, students should be able to:
  1. Understand the notion of proving a program correct
  2. Be familiar with the language of logic and set theory as applied to programs
  3. Understand how to read an axiomatic semantics for a programming language
  4. Understand how to prove that a program meets its specification

Textbooks

The following textbook will be used in this course:

Grades

Your grade will be computed as follows

Attendance Policy

Attendance will not be taken and will not count for or against you at grading time. HOWEVER, IN MY EXPERIENCE THE MOST SURE WAY TO FAIL ONE OF MY COURSES IS TO STOP ATTENDING CLASS. I OFTEN COVER MATERIAL IN CLASS THAT IS NOT IN THE TEXT BOOK, AND YOU ARE RESPONSIBLE FOR KNOWING IT FOR THE EXAM.

So, my advice is to attend class every day.

Tentative Schedule

  1. Week One: Introduction, what is a proof, propositions and predicates (Part 0 and Chapter 1)
  2. Week Two: Reasoning about equivalence (Chapter 2)
  3. Week Three: Predicates (Chapter 4)
  4. Week Four: Arrays and Assertions (Chapters 5,6)
  5. Week Five: The predicate transformer wp (Chapter 7)
  6. Week Six: Skip, abort,composition (Chapter 8)
  7. Week Seven: Assignment (Chapter 9)
  8. Week Eight: alternatives,conditionals (Chapter 10)
  9. Week Nine: Iteration (Chapter 11)
  10. Week Ten: Program Development (Chapter 13, 14)
  11. Week Eleven: Loops (Chapter 15)
  12. Week Twelve: Invariants (Chapter 16,17)
  13. Week Thirteen: Recursion, Efficiency (Chapter 18,19)
  14. Week Fourteen: Large Examples (Chapter 20)
  15. Week Fifteen: Catch-up and review

Academic Integrity

All tests and homework assignments are expected to be exclusively the work of the one student submitting the assignment. Refer to the Tiger Cub for a full statement of Auburn's academic honesty procedures.

SpecialAccomodations

Students who need special accomodations should make an appointment to discuss the Accomodation Memo during office hours as soon as possible. If scheduled office hours conflict with classes, please make an appointment. If you do not have an Accomodation Memo, but need special accomodations, contact The Program for Students with Disabilities in 1244 Haley Center (8442096V/TTY)