Abstract:
These days hardware and software systems are increasingly being used in safety and financial critical domains, such as medicine equipment, automated transportation systems and security systems. This fact makes the accuracy of their analysis very important as an uncaught system bug may endanger human life or lead to a significant financial loss. Traditionally, paper-and-pencil proof methods or computer simulations have predominantly accomplished the verification of these systems. However, these techniques do not ascertain 100% correctness and thus can be held responsible for many unfortunate incidents that happened due to an erroneous hardware or software system deployed in a safety-critical domain. Formal verification is a computer based mathematical technique for system analysis and has the potential overcome the above-mentioned limitations of traditional analysis techniques. The focus of this talk is to provide a brief overview of formal verification methods. The talk mainly targets an audience with no prior knowledge of formal methods and provides the main steps involved in applying formal verification methods for system analysis along with highlighting some of their potential application domains. Bio: Osman Hasan received the B.Eng. (Hons.) degree from the N-W.F.P University of Engineering and Technology, Pakistan, in 1997, and the M.Eng. and Ph.D. degrees from Concordia University, Montreal, Canada, in 2001 and 2008, respectively. He served as an ASIC design Engineer from 2001 to 2003 at LSI Logic Corporation in Ottawa, Canada and as a Research Associate at Concordia University, Montreal, Canada, for 18 months after his doctoral degree. Currently, he is an Assistant Professor at the NUST School of Electrical Engineering and Computer Science (SEECS) since September 2009. He is the founder and director of the System Analysis and Verification (SAVE) Lab at SEECS and his research interests include Embedded System design, Formal Methods and e-health.

Bio:
Osman Hasan received the B.Eng. (Hons.) degree from the N-W.F.P University of Engineering and Technology, Pakistan, in 1997, and the M.Eng. and Ph.D. degrees from Concordia University, Montreal, Canada, in 2001 and 2008, respectively. He served as an ASIC design Engineer from 2001 to 2003 at LSI Logic Corporation in Ottawa, Canada and as a Research Associate at Concordia University, Montreal, Canada, for 18 months after his doctoral degree. Currently, he is an Assistant Professor at the NUST School of Electrical Engineering and Computer Science (SEECS) since September 2009. He is the founder and director of the System Analysis and Verification (SAVE) Lab at SEECS and his research interests include Embedded System design, Formal Methods and e-health.