Model Checking Based on Logic Programming
C.R. Ramakrishnan
Abstract:
The short lecture series (6 hours) covers
- Introduction to Model Checking
- Temporal Logics (CTL, CTL*, LTL and Modal mu-calculus)
- Process Calculi (CCS)
- Model checking algorithms
- Tabled Logic Programming
- Tabled Resolution
- Negation and SLG resolution
- Encoding model checkers as logic programs
- CTL model checker
- Modal mu-calculus model checker
- Model checkers for processes in CCS, Synchronous CCS
- Compositional model checker for CCS and modal mu-calculus
- Beyond finite-state model checking: induction and real time systems
The lecture series describes work done in the
LMC project at Stony Brook.
The slides used in the lecture series are available in
Postscript(gzipped) and
PDF.