**This is an old revision of the document!**

Final Review

The final is on Saturday, April 22nd, from 14:30 – 17:30 in TMCB 120. One page of notes allowed (any size and any font). It consists short answer problems. Here is a comprehensive list of topics:

• Given a temporal logic formula, identify if it is LTL, CTL, or CTL* only.
• Create Kripke structures that satisfy temporal logic formulas (Homework 7)
• Write temporal logic formulas for specification expressed in english–be sure you know both CTL and LTL sub-logics (Homework 7)
• Prove (or disprove) if two temporal logic formulas are equivalent (Homework 8).
• Write LTL properties given a Promela model and specification using remoterefs (Homework 9).
• Convert arbitrary CTL formulas to formulas that only have EG, EU, and EX for operators other than normal Boolean operators (Homework 10).
• Given a Kripke structure and a set of CTL formulas, determine which states are labeled with which formulas (Homework 10).
• Play computer and show how BDDs are created and managed with the ITE given a program using the Cudd interface. Be sure to show the unique table and the recursive trees tracking the ITE calls (Homework 11 and Homework 12).
• Perform SwapVariables on a given BDD (unique table included) to replace certain variables (Homework 11).
• Create a Boolean expression for a transition relation from a simple program (Homework 13)
• Write a Boolean function describing the initial state of a system and perform forward reachability analysis using that function and a given transition relation (Homework 13 but doing it abstractly similar to class rather than BDDs).
• Perform CTL model checking using Boolean functions and fix-point computations (abstractly similar to class rather than with BDDs).

I expect the test to take 2 hours of student time.

Midterm Review

One page of notes is allowed for the exam. You are responsible for knowing the testing center hours: double check the schedule for Saturday! Below is a comprehensive list of topics on the exam. Please note that some of the topics were not covered directly by the homework, so you will want to perhaps work a few problems on your own to prepare.

• Translate if-statements and while-statements into PROMELA
• Create a PROMELA verification model to solve a problem that uses shared memory for coordinating processes
• Create a PROMELA verification model to solve a problem that uses message passing for coordinating processes. Be familiar with all the different forms of interacting with a channel including the ability to poll, insert sorted, pattern match (including the eval() function), and copy values from the channel.
• Write safety properties and create traces that violate the property.
• Write liveness properties and create traces that violate the property.
• Convert a state transition system into a Buchi Automaton
• Given a Buchi Automaton, write a regular expression that includes the $\omega$-operator that is the language detected by the Automaton.
• Compute the intersection of two Buchi automaton.
• Perform double-depth-first search to detect cycles in a given Buchi automaton. Indicate pre-order traversal numbers on both searches and show the evolution of the runtime stack.
• Given a correctness property, write a never claim to detect when the property is violated.

I expect the test to take at least 1.5 hour of student time. The total time limit on the test is 2 hours.