ECE8990-01 Automated Verification
From Ece
Contents |
Class Time and Location
TR 12:30-1:45pm
Simrall 203
Instructor
Assistant Professor
Office hours: come by at any time; call or e-mail ahead to confirm I'm available.
Textbook
- M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University press, 2nd edition, 2004.
- E. Clark, O. Grumberg, and D. Peled, Model Checking, MIT press, 2000. (optional)
Syllabus
- System Verification
- Definitions and motivation
- Methods: Simulation, Testing, Formal Verification, Model Checking, Automated Theorem Proving
- Industrial Case Studies
- Introduction to Propositional and Predicate Logic
- Propositional Logic: Natural Deduction, Semantics of PL, Normal Forms
- Predicate Logic: PL as a formal language, Proof theory of PL, Semantics of PL, Undecidability of PL
- Model Checking Linear Temporal Logic
- Syntax and semantics of PLTL
- Specifying properties in PLTL
- Basic model checking scheme for PLTL
- The model checker SPIN
- Model Checking Branching Temporal Logic
- Syntax and Semantics of CTL
- Expressiveness of CTL, CTL*, PLTL
- Specifying properties in CTL
- Model checking in CTL
- Fixed point characterization of CTL formulas
- Fairness
- The model checker SMV
- State Space Reduction Techniques
- Binary decision diagrams
- Other reduction techniques: partial order, memory managements, symmetry, bisimulation and equivalences
- Applications:
- Communication protocols
- Digital systems
- Safety critical systems
Grade Determination
To encourage hands-on experience, there will be several verification and specification assignments involving prototype-quality verification CASE tools. In addition, each student will have to complete a research project to specify and verify a larger example. Reports on the projects will be written up, and results will be presented in class.
Assignments: 60%
Project: 30%
Project presentation: 10%
Grading Scheme
A: 100-90
B: 89-80
C: 79-70
D: 69-60
F: 59-0
Assignment Submission
All assignments should be submitted electronically via the Web as either a portable document format (.pdf) or Microsoft Word (.doc) file. Click here to go to the web page that is used to submit your assignment by using 'Lab Submit Form'. Since we use 'Lab Submit Form' for our assignment submission, you should select 'Lab #1' for submitting your 'assignment #1' and so on. Click here for a FAQ about electronic submission of assignment (lab) reports.
Attendance Policy
You are required to attend all classes. Late assignments will not be accepted. Also late projects will not be accepted and a grade of zero will be given.
Prerequisites
Experience with formal methods, although helpful, is not necessary. However, the course assumes familiarity with basic mathematical structures such as relations, functions, graph theory, and finite-state machines.
Lecture Slides
Click here to get the course slides.
Academic Support
In compliance with and in the spirit of the American's with Disabilities Act (ADA), academic accommodations are made for any student with a documented disability. Students should register with the Office of Student Support Services in Montgomery Hall at (662) 325-3335 as soon as possible to better ensure such accommodations are implemented in a timely fashion and comply with their policies. Any student who believes they may need accommodations in this class are encouraged to contact Student Support Services If Student Support Services has a prescribed course of action for you with regard to this class, please visit me during office hours so we can make the proper arrangements.
Academic Integrity
Mississippi State University has an approved Honor Code that applies to all students. The code is as follows:
"As a Mississippi State University student I will conduct myself with honor and integrity at all times. I will not lie, cheat, or steal, nor will I accept the actions of those who do."
Upon accepting admission to Mississippi State University, a student immediately assumes a commitment to uphold the Honor Code, to accept responsibility for learning, and to follow the philosophy and rules of the Honor Code. Students will be required to state their commitment on examinations, research papers, and other academic work. Ignorance of the rules does not exclude any member of the MSU community from the requirements or the processes of the Honor Code. For additional information please visit: http://www.msstate.edu/dept/audit/1207A.html
Projects
There will be a project this semester.
Description coming soon.
Teaching philosophy
Textbook Use
This course is taught from the textbook and lecture slides. The textbook will be needed as it contains more detail on a subject than what is found in the slides. You will also find that just using the slides is difficult as they do not contain all of the explanation needed to understand a particular topic.
Both student and instructor share responsibility in terms of achieving the learning objectives for this course. If there is a failure in learning, try to determine where the failure is occurring - this is what any good engineer would do in debugging a problem. As a student, the first step is to TALK to your instructor if there is a problem. Without communication, it is a guarantee that the problem will not be solved. As an instructor, I am always happy to have students see me about class-related problems - this means that they are interested in removing whatever hurdles are keeping them from reaching the class learning objectives.
Instructor Responsibilities
- Answer questions! Do not stop explaining until understanding is reached. Do it either inside of class or outside of class, whatever it takes. Always be prepared to listen.
- Provide guidance as to where additional information on topics can be found.
- Provide motivation for course topics.
- Grade homeworks/quizzes in a reasonable time; assign meaningful homework problems that relate to what will be on quizzes.
- Be prepared for class. Have online notes posted that clearly explain the concepts that will be covered in the class for the day or week.
Student Responsibilities
- Ask questions! BE CURIOUS!!!! This is one of the most important aspects of an engineer - if you are not curious, then do not be an engineer. If you are simply after money, be an investment broker, speculate in real estate, win a lottery, etc.
- Investigate alternate data sources other than the professor.
- Understand the relevance of what you are being asked to learn - after all, you will be expected to perform as a real engineer in a short period of time and you need to understand how to apply this knowledge!
- Study! Read the notes covered by the instructor, ask questions if they are unclear. If you don't study, then you cannot do well on the tests. Doing well in a class is directly proportional to the effort put into studying for tests, and performing the homework/lab exercises.
Student Failure Mechanisms
What students find difficult in this course is the amount of material covered, and the pace of the coverage, not the difficulty of any one particular topic. The course concepts build on each other, so failure to understand topic 'A' means that you will not understand topic 'B' that is built on 'A'. New topics are introduced each lecture. You must keep up with the course content on a weekly basis. This means reading the material that will be covered in class BEFORE class, understanding and asking questions during the lecture, and performing the homework when it is assigned.
If you find yourself 4 weeks into the course, and completely lost (i.e, "I have not understood anything for the last 4 weeks"), then drop the course. It is a simple as that - if you are lost at that point, understanding will not come later.
You can become completely lost by not keeping up with the material and by not asking questions during lecture or office hours. Keep to your student responsibilities, and you will avoid this problem!
