Graduate Course Proposal Form Submission Detail - CDA5410
Edit function not enabled for this course.
Approved, Permanent Archive
Course Change Information (for course changes only):
- 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 Hao Zheng 9744757 firstname.lastname@example.org
- 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 -
COT 3100 Discrete Structures, CDA 3201 Computer Logic Design, EEL 4851C Data Structures, COT 4400 Analysis of Algorithms
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.
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.
- Other Course Information
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
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
- Course Concurrence Information