Apply to USF Now | Graduate Admissions | Events & Workshops | Giving to the Office of Graduate Studies

Graduate Course Proposal Form Submission Detail - CDA5410

Edit function not enabled for this course.


Current Status: Approved, Permanent Archive - 2007-11-08
Campus:
Submission Type:
Course Change Information (for course changes only):
Comments:


  1. Department and Contact Information

    Tracking Number Date & Time Submitted
    1656 2007-04-06
     
    Department College Budget Account Number
    Computer Science and Engineering EN 0-2108-000
     
    Contact Person Phone Email
    Hao Zheng 9744757 zheng@cse.usf.edu

  2. Course Information

    Prefix Number Full Title
    CDA 5410 Introduction to Computer-Aided Verification

    Is the course title variable? N
    Is a permit required for registration? N
    Are the credit hours variable? N
    Is this course repeatable?
    If repeatable, how many times? 0

    Credit Hours Section Type Grading Option
    3 C - Class Lecture (Primarily) R - Regular
     
    Abbreviated Title (30 characters maximum)
    Introduction to Computer-Aided
     
    Course Online? Percentage Online
    -

    Prerequisites

    COT 3100 Discrete Structures, CDA 3201 Computer Logic Design, EEL 4851C Data Structures, COT 4400 Analysis of Algorithms

    Corequisites

    None

    Course Description

    This course introduces basic concepts of formal verification. Topics include formal specification, algorithms, and methodologies for scalable verification. It is only for CSE majors or non-majors with permission from the instructor, not repeatable.


  3. Justification

    A. Please briefly explain why it is necessary and/or desirable to add this course.

    Verification is a major bottleneck of current software and hardware system designs. Formal verification is a new technology based on mathematic logic to formally verify a design. It has huge potential, and the computer industry is just adopting it. By pro

    B. What is the need or demand for this course? (Indicate if this course is part of a required sequence in the major.) What other programs would this course service?

    This course is for senior undergraduate and junior graduate students. It requires prior knowledge on discrete structures, logic, algorithms and data structures. It covers the basic concepts and knowledge of various formal verification topics. This course is a prerequisite of a more advanced course on formal verification.

    C. Has this course been offered as Selected Topics/Experimental Topics course? If yes, how many times?

    This course will have been offered twice as a special topic course by the end of the Spring semester, 2007.

    D. What qualifications for training and/or experience are necessary to teach this course? (List minimum qualifications for the instructor.)

    A PhD in Computer Science or Computer Engineering.


  4. Other Course Information

    A. Objectives

    This course is to introduce students to the challenges facing today's concurrent system designs, and teach students the basic concepts and methods of formal verification to address these challenges.

    B. Learning Outcomes

    1. Understand the challenges of verifying large complex concurrent systems.

    2. Understand pros and cons of simulation and formal verification approaches.

    3. Understand the concepts of formal verification and model checking.

    4. Know how to the formally specify concurrent systems using temporal logics.

    5. Understand various verification algorithms.

    6. Gain hands-on experience with formal verification tools.

    7. Know the problems of formal verification and methods addressing them.

    C. Major Topics

    1. Basic concepts of verification and model checking

    2. Modeling concurrent programs with state transition systems

    3. Formal specification using temporal logics

    4. CTL model checking

    5. LTL model checking

    6. Introduction to SMV

    7. Binary decision diagrams and symbolic model checking

    8. SAT solver and Bounded Model Checking

    9. Symbolic simulation

    10. Logic equivalence checking

    D. Textbooks

    Model Checking, E. Clarke, O. Grumberg, D. Peled, The MIT Press, ISBN: 9780262032704

    E. Course Readings, Online Resources, and Other Purchases

    F. Student Expectations/Requirements and Grading Policy

    G. Assignments, Exams and Tests

    H. Attendance Policy

    I. Policy on Make-up Work

    J. Program This Course Supports


  5. Course Concurrence Information



- if you have questions about any of these fields, please contact chinescobb@grad.usf.edu or joe@grad.usf.edu.