¶¶ÒõÂÃÐÐÉä

Ìý

Instructor: Fabio Somenzi

Office: ECOT348Ìý

E-mail:Fabio@Colorado.EDUÌý

Office Hours: Tuesday, 3:30-4:30 pm, Thursday 10:00-11:00 am, or by appointment

Course Description

Today's complex hardware and software systems are difficult to verify. On the other hand, the cost of shipping defective products is often prohibitive. In the case of safety-critical applications, the cost may even be in terms of human lives. These factors have spurredinterest in formal methods for the verification of hardware and software. The last few years have seen the successful deployment offormal methods in many projects, and the launch of several tools based on them.

Among the formal techniques applied to the verification of hardware, model checking has proved the most popular. In model checkin gone is given a model of a system and a set of properties that should be satisfied. The model is reduced, if necessary, to a small, finite-state model, and state exploration techniques are applied to check the properties.

Even a comparatively small model can have a huge number of states. Therefore, efficient techniques for state exploration are mandatory for successful application of model checking. Of particular interest are the so-called symbolic techniques, in which sets of states and transitions are represented by their characteristic functions.

This course provides a comprehensive introduction to model checking. The emphasis is on fundamental techniques and hardware verification, but software verification will be discussed as well. We shall initially discuss first-order languages to establish a logical foundation for the rest of the course. We shall discuss the specification of systems and properties. In particular, we shall introduce temporal logics.The model checking algorithms for the most popular temporal logics rely on the computation of fix points and on the translation of properties into special automata called omega-regular automata. We shall review both processes, and thus formulate a model checking algorithm for a large class of properties.As mentioned above, the number of states of a model can be very large. The exponential dependence of the number of states on the size of the model is known as the state explosion problem. The second part of the course will therefore concentrate on techniques to combat this problem. Our emphasis will be a data structure named Binary Decision Diagrams (BDDs) and tools called SAT solvers. BDDs represent Boolean functions. Boolean functions, in turn, can be used to represent sets of states and transitions. The advantage is that even very large sets (e.g., 10**100 elements) may have compact representations.

We shall examine BDDs and SAT solvers in depth, by studying the basic algorithms and the operations that are at the core of symbolic model checking. SAT solvers can be used to find paths in complex transition systems or to mechanize induction proofs. Even the shrewdest BDD and SAT techniques, however, cannot solve by themselves the state explosion problem. Therefore, we shall consider the important topic of abstraction. Abstraction consists of deriving a simpler model from the one given, in such a way that the properties of interest can be proved (or disproved) for the original system while working on the reduced system. Various techniques have been devised for abstraction. They may map a finite system to a smaller one, or even an infinite system to a finite one. The latter is commonly done in software verification. We shall review some of the most widely used.

Homework, Exams and Grading

Grading will be based on homework, a programming project, one mid-term exam and the final exam. Both exams will be take-home exams. Homework will be assigned often and in general you will have one week to do the assignment. The programming project will be assigned by early November and due at the start of the last week of classes.The final grade is determined as follows:

• 25% homework
• 25% programming project
• 20% midterm
• 30% final exam.

Assignments, solutions, course material, and announcements will be posted here on Canvas. The final exam is due on Wednesday December 18 at 7 pm.

Schedule Conflicts, Special Arrangements, and Emergencies

For all special arrangements, contact the instructor at your earliest convenience. The sooner you act, the easiest will be to find a suitable solution.

Honor Code

A complete description of the honor code can be found here.

To summarize: "Violations of the Honor Code are acts of academic dishonesty and include but are not limited to plagiarism, cheating, fabrication, aid of academic dishonesty, lying to course instructors, lying to representatives of the Honor Code, bribery or threats pertaining to academic matters, or an attempt to do any of the aforementioned violations."

Dealing with honor code violations is extremely unpleasant for all parties involved and may have very serious consequences for the offenders. Stay clear of trouble. Your education will thank you for doing so.