mc-tutorial

Model CheckingJavier Esparza and Stephan MerzLab. for Foundations of Computer Science, University of EdinburghInstitut fur¨ Informatik, Universitat¨ Munchen¨Program9:00–10:00 Basics 14:00–15:30 AbstractionA bit of history BasicsA case study: the Needham Schroeder protocol Predicate AbstractionLinear and branching time temporal logics 15:30–16:00 Coffee Break10:00–10:30 Model checking LTL I 16:00–17:30 Infinite state spacesThe automata theoretic approach Sources of infinitySymbolic search10:30–11:00 Coffee BreakAccelerations and widenings11:00–11:30 Model checking LTL IIOn the fly model checkingPartial order techniques11:30–12:30 Model checking CTLBasic algorithmsBinary Decision Diagrams12:30–14:00 Lunch2BasicsA bit of historyA case study: the Needham Schroeder protocolLinear and branching time temporal logics3A bit of historyGoal: automatic verification of systemsPrerequisites: formal semantics and specification language In the beginning there were Input OutputSystems . . .Total correctness = partial correctness + terminationFormal semantics: input output relationSpecification language: first order logic. Late 60s: Reactive systems emerge . . .Reactive systems do not “compute anything”Termination may not be desirable (deadlock!)Total correctness: safety + progress + fairness . . .Formal semantics: Kripke structures, transition systems ( automata)Specification language: Temporal logic4Temporal logic Middle Ages: analysis of modal and ...