E0 223 Verification

• Course outline
  • Temporal Logic based verification:
    • Introductory automata concepts
    • Buchi automata
    • Linear Temporal Logic (LTL)
    • Modelling systems
    • Computation Tree Logic (CTL)
    • Tools: Spin, SMV
  • Verification of real-time systems
    • Timed automata
    • Modelling real-time systems
    • Tools: Uppaal, Kronos
• Texts and other material
  • Clarke, Grumberg, Peled: Model Checking
    
  • Berard, Bidoit, Finkel, et al: Systems and Software Verification
  • Wolfgang Thomas: Automata on Infinite Objects, in Handbook of Theoretical Computer Science, Elsevier 1990.
  • Madhavan Mukund: Finite-state Automata on Infinite Inputs
  • Courcoubetis et. al: Memory Efficient Algorithms for the Verification of Temporal Properties
  • Spin website: spinroot.com.
  • Randy Bryant: Graph-Based Algorithms for Boolean Function Manipulation.
  • SMV: tared binaries (also contains html version of tutorial and language reference. Hard copies available with me.)
  • Uppaal binaries.
• Assignments
  • Assignment 1
  • Assignment 2
  • Assignment 3
  • Assignment 4
• Proposed weightage for evaluation:
  • Mid-semester Exam: 20%
  • Assignments (Lab + written): 40%
  • Final Exam: 40%
• Current meeting schedule: Tue & Thu, 2:00pm, in CSA Seminar Room.
• Exam Schedule:
  • Mid-semester Exam: 11:00 am Monday, 24th Feb 2003.
  • Final Exam: 10:00 am Tuesday 22nd April 2003.