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 ;