This page is quite out of date.
September 2003:
CS 245 - Logic and Computation
Course calendar description: Formal logic. Proof systems and styles.
Rudimentary model theory. Formal models of computation. Logic-based
specification. Correctness proofs. Applications in software engineering
September 2003:
CS 745 Reading - Computer-Aided Verification
(grad course, co-taught with Professors Aagaard, Atlee, Thistle, Trefler)
Description: To deal with the complexity of the software and hardware
in today's
computer-based systems, we need ways of analysing requirements
and designs for properties such as correctness and safety. Formal
methods, which are techniques based on logical reasoning and mathematical
modelling, provide some of the underlying theory and techniques for this
analysis. These computer-aided verification methods are gradually
making their way into CASE and CAD tools. This course introduces the
theory and practice of computer-aided verification for the design and
analysis of systems. Topics covered include: formal specification and
logic, model checking, mechanical theorem proving, decision procedures,
integration of these techniques with design practices, and applications
of these approaches to requirements, software, hardware, and protocols.
January 2003:
CS 245 / SE 112 - Logic and Computation
Course calendar description: Same as above.
September 2002:
CS 745 - Computer-Aided Verification
(grad course)
Course calendar description: Same as above.
January 2002:
SE 112 - Logic and Computation (undergrad 1B)
Course calendar description: Same as above.
September 2001:
CS 745 - Computer-Aided Verification (grad course)
Description: Same as above.
Send questions or comments to Nancy Day
< nday@cs.uwaterloo.ca
>