Site Map | College of Engineering | UC Davis | MyUCDavis

ECS 261 PROGRAM VERIFICATION (4) I

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%)

Catalog Description:
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:

  1. Review of Propositional and First-Order Logic
    1. Interpretations
    2. Relevance of first-order logic to automated deduction
    3. Limitations of automated deduction
  2. Symbolic Execution
  3. Techniques Suited to Iterative-Style Programming
    1. Floyd-Hoare methods
    2. Inductive assertions
    3. Subgoal induction
    4. Intermittent assertions
    5. Procedure calls
  4. Methods from Denotational Semantics
    1. Cpo's least fixed points
    2. Fixpoint induction
  5. Proof of Termination for Iterative Programs and Recursive Programs
  6. Introduction to Modern and Advanced Topics in Verification
    1. Dynamic logic
    2. Verification of nondeterministic and concurrent programs
    3. Verification of functional programs
    4. Verification of logic programs
    5. Verification of realtime programs

Textbook:
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

Back to Course Descriptions