Spring 2007

Aims: The course will train students in the principles and techniques of validating and verifying complex software systems. The training will be at an intellectually demanding level and will cover not only the state-of-the practice in validation and verification, but also the most significant trends, problems and results in validation and verification research.

Learning Outcomes: On completion of the course unit, the successful student should have a good knowledge and understanding of basic notions of correctness, consistency, faults and failures, testing and execution trace analysis. The successful student should also be able to understand the use of logic as a formal language for specification of systems, to understand the use of the main verification techniques used in symbolic model checking, to understand the architecture and be able to use a main tool (such as SMV) to verify simple systems. Further, successful students will be able to appreciate the limitations of the current tools and have insights in ongoing advanced research topics to overcome them.