Formal Methods
School of Electrical Engineering & Computer Science (SEECS),
National University of Sciences & Technology (NUST),
Sector H-12, Islamabad 44000,
Pakistan
Instructor: Dr. Osman Hasan
Office Hours: By Appointment
Course Description:
In
today's world, hardware and software systems are increasingly being used in
safety-critical domains, like medicine, transportation, banking and military. An
uncaught system bug in systems designed for these application domains can
result in disastrous consequences including the loss of human life and thus
approximate analysis techniques, like software testing, should not be relied
upon for their analysis. This course is about an alternate analysis approach;
Formal Methods. Which are computer based mathematical analysis techniques for
the specification and verification of systems. The mathematical nature of
Formal Methods ensures absolute correctness of software and hardware designs
and thus their usage has been integrated in the industrial design flows of all
critical systems. This course is particularly focused on introducing the widely
used formal methods, their underlying logical theories and their main strengths
and weaknesses.
Text Books
-
Michael Huth and Mark Ryan, Logic in Computer
Science: Modelling and Reasoning about Systems. Cambridge University Press
(Second Ed.) (2004)
- M.
J. C. Gordon, T. F. Melham, Introduction to HOL: A Theorem-Proving Environment
for Higher-Order Logic, Cambridge University Press (1993)