This page contains information for students who consider to devote their final term project to a subject in theoretical computer science. If you have any question, please contact one of us. See the homepage of our group for our email addresses.
Contents of this page:
The research of the theoretical computer science group
at VU is concerned with
validation of protocols,
verification of specifications and programs,
rewriting systems (first-order term rewriting,
graph rewriting, higher-order term rewriting),
lambda calculus, type theory,
structural operational semantics.
Knowledge of (some of) the following courses
is recommended background knowledge for a
final term project in theoretical computer science:
Final term projects in verification.
Part of the research at the theoretical computer science group
is devoted to the verification of distributed and embedded systems
and communication protocols. For this purpose we study and develop
formal techniques for the unambiguous description, design and
documentation of full software systems. A main vehicle forms the language
based on process algebra in combination with abstract data types;
others are timed automata
model checkers (CADP,
and theorem provers (PVS,
Coq, µCRL prover).
We work with a wide range of analysis techniques and resources
to prove that programmed systems exhibit their expected functionality.
We employ methods from algebra and logics, as well as term-rewriting.
For the analysis of data and processes, dedicated tools for proof
checking, state-space analysis and reduction, simulation, and
testing are used. In order to assess the viability of various
techniques and tools, we carry out experiments in the realm of
communication and security protocols, distributed algorithms, and
embedded and hybrid control systems.
Our ongoing research work frequently includes challenges that can be
assigned to students as graduation projects. If you are interested,
you are invited to contact
Wan Fokkink at the email address
given below. Current projects include the following topics:
Subjects for Master's theses:
Final term projects in rewriting.
Roel de Vrijer
(firstname.lastname@example.org) for further information.
Some possibility in higher-order rewriting:
Final term projects in proof checking.
F. Baader and T. Nipkow
Cambridge University Press 1998/1999.
Higher-Order Recursive Path Orderings "à la carte"
Available via this page.
Well-founded recursive relations. Available via this page.
On termination of higher-order rewriting
Available via this page
Final term projects in process algebra and structural operational semantics.
(email@example.com) for further information.
Some master's theses in tcs.
To get an impression of a master's thesis in
theoretical computer science, please have a
look at the theses that were written the
last years (this is an incomplete list).
Infinitary Rewriting in Coq, August 2010. (Coq formalisation)
A virtual shared disk on distributed redundant storage, VU technical report IS-TI-010, April 2010.
Design and analysis of UniPro protocols for mobile phones, VU technical report IS-TI-009, July 2009.
On modal characterizations and turning GSOS rules into equations, VU technical report IS-TI-008, January 2009.
Fault tolerant rings: creation and maintenance, VU technical report IS-TI-007, October 2008.
A formal analysis of the RIES internet voting protocol VU technical report IS-TI-006, April 2007.
Reduction algorithms on linear process equations, VU technical report IS-TI-005, October 2005.
Well-foundedness of the higher order recursive path ordering in Coq, VU technical report IR-TI-004, August 2004.
Verification of behavior protocols VU technical report IR-TI-003, August 2003.
Well-foundedness of RPO in Coq, VU technical report IR-TI-002, August 2003.
Quantum complexity classes, VU technical report IR-TI-001, August 2003.
A story of meaningless terms, VU technical report IR-502, August 2002.
Networks of rewriting systems VU technical report IR-501, August 2002.
Structural operational semantics and bounded nondeterminism, VU technical report IR-500, July 2002.
Modal logic in Coq, VU technical report IR-488, May 2001.
A coalgebraic approach to lambda calculus, VU technical report IR-478, September 2000.
Back to the homepage of theoretical computer science.