Sample exam questions (nonexhaustive list) - temporal logic: define operator <...>, give the fixpoint formula for operator <...>, write a symbolic algorithm for checking formula <...>; translate the following natural language spec. to a temporal logic formula Example: after every p, q is possible, and if it happens, r always follows. - timed systems: define a timed automaton; model the following system as a timed automaton; write an execution trace / calculate the timed zones for the execution of the following automaton; - logic: define propositional / predicate logic; interpretation ; deduction ; logical implication ; consistency ; completeness ; Example: is the following formula satisfiable? \$! E x [R(x)] /\ A x E y [R(x) \/ S(y)] /\ E x A y [S(y) -> R(x)] (where ! = not, E = \exists, A = \forall) - program analysis: write Hoare rules; formulas for weakest preconditions; Example: weakest precondition for *p == x after { *p = 4; *q = 5; } explain worklist algorithm; write a static analysis for the following property; explain verification w/ predicate abstraction; widening and narrowing - define / relate language inclusion / simulation / bisimulation - security: define Dolev-Yao assumptions and intruder; give examples of rules in BAN logic; explain what the following protocol does and model it in BAN logic ;