[Prev][Next][Index][Thread]

PhD studentship

Dear Colleagues,

We would be grateful if you brought this to the attention of potential
students.

---

Department of Computer Science
University of Warwick
England

PhD studentship
Scalable Software Model Checking Based on Game Semantics

A three-year PhD studentship funded by the Engineering and Physical
Sciences Research Council is available from October 2003.  It covers
academic fees, and living expenses at the following rates: GBP 9,000
(2003/04), GBP 10,500 (2004/05), GBP 12,000 (2005/06).

* Project summary

Model checking has been a highly successful approach to verification of
hardware and protocols.  Recently, model checking of software has become
an active and important area of research and application.  In contrast to
hardware and protocols, software is often highly structured, and contains
objects, higher-order computation, complex control mechanisms, pointers,
concurrency, and other features.  Although impressive tools have been built,
a number of substantial challenges remain for software model checking.

One of the main breakthroughs in theoretical computer science in the past
decade has been the development of game semantics, which has produced
the first accurate models for a variety of programming languages and
logical systems.  Founding software model checking on game semantics has
the potential to overcome most of the remaining challenges, because
the models are compositional in the style of denotational semantics,
yet have clear operational content.

We propose contributions to theory and practice of the novel research
direction of software model checking based on game semantics.  Our main goal
is to enable compositional verification of programs and specifications which
contain large, polymorphic or infinite data types.  This has not been
addressed so far, but is necessary for the approach to scale to industrial
software.

The studentship will be supervised by Dr R Lazic, within the Theory and
Practice of Programming research group led by Prof D Peled.

Collaboration is planned with the Foundations of Computation research group
at Oxford, and with Formal Systems (Europe) Ltd.

* Requirements and application

You should have at least a II.1 degree in Computer Science or Mathematics,
or equivalent.  You need to have experience of at least one of:
- semantics of programming languages,
- automata theory,
- process algebra,
- category theory.

Further information is available at:
http://www.dcs.warwick.ac.uk/people/academic/Ranko.Lazic/res/phd.html

Informal enquiries by e-mail are welcome:
Ranko.Lazic@dcs.warwick.ac.uk

You can apply on-line, stating the project title in Question 13:
http://www.warwick.ac.uk/study/postgraduate/

Closing date: 11 July 2003.