CS357
Software Verification
2011-2012
Topics
Theorem proving:
natural deduction for propositional logic and predicate logic
Program verification:
using Hoare logic to specify and verify programs
Model checking:
Temporal logic (LTL and CTL) and their associated model-checking algorithms
In the labs we'll be using
Coq
,
NuSMV
and
Spec#
Recommended text
Logic in Computer Science: modelling and reasoning about systems
(second edition)
by Michael Huth and Mark Ryan, Cambridge University Press, 2004
ISBN: 052154310X
Timetable:
Lectures:
Mondays at 15.00 in CSR, Thursdays at 11.00 in CS1
Labs:
Tuesdays 12.00-14.00 in Lab 3
More course information will be available through the
university's moodle system.
James Power
,
Dept. of Computer Science
,
NUI Maynooth
Last revised: 14 September 2011