This track aims at Computer Science students with a general interest in
the application of formal methods in computing, concurrency and the
design and verification of software systems. Some theoretical
disciplines that play a central role are term rewriting, process
algebra, distributed algorithms and type theory. Foundational
disciplines include logic, recursion theory and complexity.
All these topics have a wide range of applications, of which we mention
just a few. Tools developed from process algebra are used in protocol
validation. Term rewriting is used in the execution of equational
specifications and lies at the basis of functional programming and the
analysis of infinitary processes. Distributed algorithms are of central
importance for the efficient use of concurrent systems. Logic and type
theory form the basis of proof checking, used in software verification.
In all of the above areas courses are offered. To mention a few
examples: Distributed Algorithms, Logical Verification, Protocol
Validation, Term Rewriting Systems, Concurrent System Design by
Abstraction. The programme can be enhanced by choosing one or more
appropriate mathematics courses.
Note: Every programme, including the choice of optional courses, has to
be discussed and agreed upon with the master coordinator or a personal
mentor and approved by the Examination Board.
dr. F. van Raamsdonk
K room T-446
T +31 (0) 20 598 7710