I am a full time Professor in the
department of Computer Science, University at Buffalo,
NY, USA. I earned my Ph.D. degree in Computer Science from the
University of Utah in 1989.
My research interests are dynamic analysis and visualization in a state-of-the-art execution environment for Java called JIVE; program analysis and applications of constrained objects, and constraint-based design; identification, tracking, and retrieval in cyber physical spaces based upon camera networks and biometric sensors; and, more recently formal methods in software and safety-critical systems.
Links: DBLP, Google Scholar
Formal methods involve the use of formal specification languages and formal verification techniques with the goal of providing increased assurance/rigorous guarantee of the correctness of software or hardware systems. Formal specification involves the use of mathematical and logical formulae to state the properties of interest, while formal verification make use of theorem proving or model checking techniques to prove that the system satisfies the properties or to provide a counter-example. In the area of computer security, formal methods were first applied to show the correctness, or the lack thereof, for authentication protocols. Over the years, formal methods have been applied to specify and reason about security properties at the various levels: applications, programming languages, operating systems, networking, internet/web, and databases. This course will provide an overview of formal methods and illustrate their use through a variety of examples.