Lecture: 3 hours
Discussion: 1 hour
Prerequisite: Math 125 or Philosophy 112 or familiarity with first-order logic. Knowledge of an iterative and functional programming language.
Grading: Letter; based on homework (25%), midterm (25%), final (25%) and project (25%)
Methods of proving correctness of programs with respect to formal specifications, with attention to those suited for employing automated deduction. Logic background, symbolic execution, techniques suited to iterative programming, methods from denotational semantics, termination, dynamic logic and proofs of concurrent programs.
Expanded Course Description:
Selected from the current literature.
Engineering Design Statement: The students will apply the principles of verification to verify a small albeit realistic system, e.g., an interpreter, a compiler, a small operating system, a controller for a realtime system.
ABET Category Content:
Engineering Science: 3 units
Engineering Design: 1 units
Instructor: K. Levitt
Prepared by: K. Levitt (Feb. 1997)
THIS COURSE DOES NOT DUPLICATE ANY EXISTING COURSE
Last revised: 2/97