Skip to main content
KBS_Icon_questionmark link-ico
Study Abroad at King’s
Study

Go to…

Formal Verification

Key information

  • Module code:

    6CCS3VER

  • Level:

    6

  • Semester:

      Autumn

  • Credit value:

    15

Module description

Aims and Learning Outcomes

This module aims at providing an in-depth introduction to different state-of-the-art methodologies of Formal Verification and the applications of those methodologies to formally model and reason about algorithms, software, systems, and protocols.

On successful completion of this module, students will:

At the end of the course students will be able to:

  • Define a range of formal models
  • Formalise problems and specify properties to be verified
  • Apply different methods and algorithms for verification

Syllabus

An indication of the types of topics: 

  • temporal logic: CTL and LTL, Buchi automata
  • Explicit model checking
  • BDDs and model-checking with BDDs
  • symbolic model checking
  • SAT and model-checking with SAT
  • Security verification
  • hybrid automata
  • hybrid system verification
  • applications of model checking to hardware, software, and protocols verification
  • Modelling and functional programming in higher-order logic: recursion, algebraic data types, and high-order functions
  • Interactive proofs in higher-order logic: mathematical induction, structural induction, and computation induction
  • Proof automation in higher order logic
  • Applications of interactive theorem proving to formal verification

Assessment details

Please note: The below assessment details for the 2024/25 academic year may be updated. The confirmed details will be available on the Student Handbook and on the module KEATS page at the beginning of the semester.

  • 100% Examination

Semester 1 only study abroad students will be required to take this exam in an alternative assessment format in the January exam period.

Full year study abroad students will be required to take this exam in person in January.

Subject areas

Department

Module description disclaimer

King’s College London reviews the modules offered on a regular basis to provide up-to-date, innovative and relevant programmes of study. Therefore, modules offered may change. We suggest you keep an eye on the course finder on our website for updates.

Please note that modules with a practical component will be capped due to educational requirements, which may mean that we cannot guarantee a place to all students who elect to study this module.

Please note that the module descriptions above are related to the current academic year and are subject to change.