Graduate Studies Reports Access
Graduate Course Proposal Form Submission Detail - CDA5410
Tracking Number - 1656
Edit function not enabled for this course.
Approved, Permanent Archive - 2007-11-08
Course Change Information (for course changes only):
- Date & Time Submitted: 2007-04-06
- Department: Computer Science and Engineering
- College: EN
- Budget Account Number: 0-2108-000
- Contact Person: Hao Zheng
- Phone: 9744757
- Email: firstname.lastname@example.org
- Prefix: CDA
- Number: 5410
- Full Title: Introduction to Computer-Aided Verification
- Credit Hours: 3
- Section Type: C -
Class Lecture (Primarily)
- 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
- Abbreviated Title (30 characters maximum): Introduction to Computer-Aided
- Course Online?: -
- Percentage Online:
- Grading Option:
R - Regular
- 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.
- 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
- 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.
- 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.
- 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.
- 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.
- 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.
- 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
- Textbooks: Model Checking, E. Clarke, O. Grumberg, D. Peled, The MIT Press, ISBN: 9780262032704
- Course Readings, Online Resources, and Other Purchases:
- Student Expectations/Requirements and Grading Policy:
- Assignments, Exams and Tests:
- Attendance Policy:
- Policy on Make-up Work:
- Program This Course Supports:
- Course Concurrence Information: