Graduate Studies Reports Access

Graduate Course Proposal Form Submission Detail - CDA5410
Tracking Number - 1656

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:

---

Detail Information

1. Date & Time Submitted: 2007-04-06
   
2. Department: Computer Science and Engineering
   
3. College: EN
   
4. Budget Account Number: 0-2108-000
   
5. Contact Person: Hao Zheng
   
6. Phone: 9744757
   
7. Email: zheng@cse.usf.edu
   
8. Prefix: CDA
   
9. Number: 5410
   
10. Full Title: Introduction to Computer-Aided Verification
    
11. Credit Hours: 3
    
12. Section Type: C - Class Lecture (Primarily)
    
13. Is the course title variable?: N
    
14. Is a permit required for registration?: N
    
15. Are the credit hours variable?: N
    
16. Is this course repeatable?:
    
17. If repeatable, how many times?: 0
    
18. Abbreviated Title (30 characters maximum): Introduction to Computer-Aided
    
19. Course Online?: -
    
20. Percentage Online:
    
21. Grading Option: R - Regular
    
22. Prerequisites: COT 3100 Discrete Structures, CDA 3201 Computer Logic Design, EEL 4851C Data Structures, COT 4400 Analysis of Algorithms
    
23. Corequisites: None
    
24. 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.
    

25. 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
    
26. 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.
    
27. 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.
    
28. 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.
    
29. 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.
    
30. 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.
    

31. 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
    

32. Textbooks: Model Checking, E. Clarke, O. Grumberg, D. Peled, The MIT Press, ISBN: 9780262032704
    
33. Course Readings, Online Resources, and Other Purchases:
    
34. Student Expectations/Requirements and Grading Policy:
    
35. Assignments, Exams and Tests:
    
36. Attendance Policy:
    
37. Policy on Make-up Work:
    
38. Program This Course Supports:
    
39. Course Concurrence Information:
    

---

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