First Session (15/4/02) ------------- 1: Probablistic Abstraction possibilistic + probablistic abstraction doable; good in \forall Bad: functional abstraction, but this is usually tractable 2: Probablistic Model Checking of IEEE 802.11 Wireless LAN WLAN { Need collision avoidance { Uses randomised exponential backoff Discrete probablistic choice over bounded interp[?] variables Urgent events make life harder; need lazt automata [talk was rushed & still overran a lot] Second Session -------------- 3: Parallelisation of Model Checking Better to keep amount of shared queue fairly small (a bit less than mean branching degree) 4: Logic Programming and Partial Deduction for Verification of Reactive Systems PROLOG is not dead! Finite State MC using Tabled LP; tables are built-in memoization + Simple declarative program Correct for finite + infinite systems Connect to other analysers + transformers Easily extendible Infinite MC by partial evaluation Always safe, but might say "don't know" Finite: XTL fairly good (SPIN better) Infinite: Ecce *good* (but awful on finite) 5: Reactive Types for Dataflow-Oriented Component-Based Design Nested Clocks (didn't look like types to me!) 6: Crash in Program Logic Crash as form of non-termination in Hoare Logic Need 3-valued logic to reason about crashes Third Session ------------- 7: Functional Proof Decompositions [INVITED TALK] Units of work may be obvious Units of work have limited interaction property | V decomposition Divide into units of work | | | V V V parameterisation Case splitting | | | V V V abstraction Abstract interpretation | | | V V V model check "Circular" Assume/Guarantee (identify units of work) + p --> q equiv_{LTL} ¬(p Until ¬q) (if we assume p does the right thing, q won't go wrong) + + p --> q q --> p ---------------------- Gp /\ Gq Ref. Model e.g. programmers model | | |p |q Refinement relations (TL) V V +---+ ,->| A |--. | +---+ | | | "circular" proof | +---+ | `--| B |<-' +---+ A + B perform a "unit of work" Temporal Case Splitting (identify resources used) Abstract Interpretation (strips cases not relevant) \forall i.G((w=i) => \phi) -------------------------- G\phi + \phi --> ((w=i) => \phi) By function, then structural if necessary, then MC Look at what computations are being performed Dividing proof into "units of work" can be faster way to reduce problem to a decidable theory, but choosing "unit of work" requires insight (e.g. in Lamport's bakery algorithm for mutual exclusion, unit of work is a ticket number!) Not so useful when complex data Fourth Session -------------- 8: Dual Transition PetriNet Models: FS MC + IS MC DTPN v.tight control + data flow representation safe DTPN models -> SMV k-bounded DTPN -> CLP unbounded DTPN -> CLP [??] 9: Simulations in Rebeca OO model for reactive systems suitable for formal verification 10: Localizing Model Checking by Analysing Transitions For where dependencies are not obvious Fifth Session ------------- 11: Towards Specification as Refinement in Timed Systems /\ /..\ /....\ /....<-------- unrealizable /........\ ---------- \# #/ \# <-------- syntactic procs \____/ \##/<------- livelock \/ 12: Property-Based Compression Strategies Try to compress big things first when doing compression of parallel 13: Implementing Data-Dependencies: Symbolic Op Semantics for CSP_m , Lazic/Roscoe-style data independence uses typed \lambda calculus CSP_m/FDR not really compatable Sixth Session (16/4/02) ------------- 14: Accelerating UPPAAL [INVITED TALK] Plant (continuous) .... +--------------+ ........ sensors | +----+ | .. __.. ---------->| |Ta+----+ | .. / .. | +--|Ta+----+ | ..__/ .. actuators | +--|Task| | ........ <----------| +----+ | | .... +--------------+ |user-supplied A | |models Code Gen| |Models of tasks (automata V | V +------------------------------------+ | timed automata models | +------------------------------------+ Timed Automata ,---. actions ,---. | n |----------------->| m | `---'x<=5&y>3 x:=0`---' x,y are clocks Also have location invatiants (on clocks) which must be satisfied for state to be permitted Also have discrete variables to make modelling easier Cute GUI! (See paper for details of how UPPAAL is actually accelerated) Seventh Session --------------- 15: SAW: The Spatial Assertion Workbench Pointers are problematic SAL (language) * is spatial conjunction; corresponds to "heap splitting" Frame rule: {P} C {Q} ------------------- {P * R} C {Q * R} (x |-> 42,nil) * (y |-> 42,nil) x,y not aliases (x |-> 42,nil) /\ (y |-> 42,nil) x,y *must* be aliases (x |->a,y) * (y |-> b,x) 2-node cyclic list MC (using heap as graph) 16: Five Ways to Use Induction and Symmetry in MC Reasoning about networks of similar processes M(P_k) |= \phi State-space explosion, case explosion -> symmetry Lack of inference, generalisation -> induction 17: Logical Analysis of Feature Integration [Very math heavy and far too dry; couldn't understand enough to make proper notes] Eighth Session -------------- 18: Analysing Protocols Subject to Guessing Attacks Good talk + paper; see paper for details (sections 3+4 ignored) 19: Verifying Authentication Protocol Implementations Use CSP w. standard rules to handle crypto A <---> Enemy <---> B ^ | Rank function v S Watch out for perfect encryption assumption Sometimes {{m}_k_1}_k_2 = {{m}_k_2}_k_1 RSA, xor or {m,{m}_k} |- k xor Coping with xor; msg concat -> rank concat Construct rank function to return bit vectors RANK+ = all bits 1 RANK- = contains 0 20: Authentication Protocols using One-Way[ Functions: a PVS Analysis Using dependent types for nonces Ninth Session ------------- 21: HOL Case Study: Verifying Probabilistic Programs Must be able to formalize prob. spec (use infinite strings of "random" boolean values) 'e: P(P(|B^\inf)), |P : 'e -> |R prob_prog: |N -> |B^\inf -> {succ,fail} * |B^\inf show chance of failure v. small ^ f : 'a -> 'b | V f : 'a -> |B^\inf -> 'b * |B^\inf ^ prob. that f(a) meets spec B:'b -> |B B . {s | fst(f a s) = b} Prob. MC better in automatic contexts, but only finite Theorem Provers like HOL can tackle infinite, but interactive COQ better at execution, but has problems with measure theory 22: Using PVS to Support a RT Refinement Calculus Recursive Refinement seems cute way of looping 32: Investigation into Proof Automation for SPARK Approach to High Integrity Ada SPARK is Ada subset (eliminates ambiguities and inconsistencies) Supports code annotations Static analysis (data flow, info flow + formal verification) Correctness-by-construction (go from Z -> SPARK) Proof Plans = Tactics (like LCF) + Methods + Critics (AI technique from late 80s) Try to create "big steps" to simplify user's work user ^ | ,--->conjectures-----. | | | +--V---|--------------------V------+ | +---------+ tactic +---------+ | | | planner |--------->| checker |-----> proof | +---------+ +---------+ | +------|--------------------^------+ | | `------>theory-------' Much of proof plan can be reused Tenth Session ------------- [MISSED TO CATCH TRAIN HOME]