From: Andrew Butterfield <Andrew.Butterfield@cs.tcd.ie>
Cc: agents@cs.umbc.edu, appsem@lists.tcs.ifi.lmu.de,
caml-list@inria.fr, comlab@comlab.ox.ac.uk,
coq-club@pauillac.inria.fr, lfcs-interest@dcs.ed.ac.uk,
logic-list@Helsinki.FI, nvti-list@cwi.nl,
petrinet@informatik.uni-hamburg.de, procos@jiscmail.ac.uk,
prog-lang@diku.dk, seworld@cs.colorado.edu,
theory-logic@cs.cmu.edu
Subject: Funded PhD position: formalising hardware/software interface
Date: Thu, 22 May 2008 09:44:30 +0100 [thread overview]
Message-ID: <4835326E.4090806@cs.tcd.ie> (raw)
In-Reply-To: <000c01c8bbdd$03b095d0$b50112ac@nb5279>
3-year funded Ph.D. position
Formalising the Interface between Software and Hardware (FISH)
https://www.cs.tcd.ie/Andrew.Butterfield/FISH/
Start Date: September/October 2008
Team:
Foundations and Methods Group,
Software Systems Laboratory,
Trinity College Dublin
Supervisor: Andrew Butterfield Andrew.Butterfield@cs.tcd.ie
Summary
The aim of this project is to investigate the modelling of the interface
between
hardware and software, with particular emphasis on Flash Memory devices.
The motivation for this work is to be able to contribute to a formally
verified
model of a POSIX-aware file-store implemented with flash memory,
and so suitable for mission-critical data-collection applications
such as space probes.
This is part of a pilot project currently under way in the Grand Challenge
on Dependable Systems Evolution.
The research will use the techniques of the Unifying Theories of
Programming (UTP),
and recent work on the language "Circus", and a variant called
"slotted-Circus",
to explore the theory and practise of reasoning about the correctness
of software at the hardware interface level, incorporating techniques
for reasoning about the correctness in the face of certain classes of
failure
whose occurrence is probabilistic and non-determinisitic.
We seek a student with an interest in modelling and verification,
with experience of at least one formal method (Z, VDM, B, CSP, pi-Calculus)
and skills with discrete mathematics, predicate calculus and theorem
proving.
The candidate should have a good background in computer science, with
a good Bachelors or MSc degree in Computer Science, Mathematics or a
similar
area.
The funding covers fees, plus a stipend of 17,000+ euros.
Applications:
Send applications, by email to
mailto:Andrew.Butterfield@cs.tcd.ie?Subject=FISH,
containing:
1. Detailed CV
2. Contact details for at least two referees
3. A clear statement as to why you would be suited for this research
project.
See the project website for further details
https://www.cs.tcd.ie/Andrew.Butterfield/FISH/
--
--------------------------------------------------------------------
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Foundations and Methods Research Group Director.
School of Computer Science and Statistics,
Room F.13, O'Reilly Institute, Trinity College, University of Dublin
http://www.cs.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------
prev parent reply other threads:[~2008-05-22 8:44 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2008-05-22 7:25 Vacancy Announcement: two post-doctoral researcher positions at UNU-IIST Wang Xu
2008-05-22 8:44 ` Andrew Butterfield [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=4835326E.4090806@cs.tcd.ie \
--to=andrew.butterfield@cs.tcd.ie \
--cc=agents@cs.umbc.edu \
--cc=appsem@lists.tcs.ifi.lmu.de \
--cc=caml-list@inria.fr \
--cc=comlab@comlab.ox.ac.uk \
--cc=coq-club@pauillac.inria.fr \
--cc=lfcs-interest@dcs.ed.ac.uk \
--cc=logic-list@Helsinki.FI \
--cc=nvti-list@cwi.nl \
--cc=petrinet@informatik.uni-hamburg.de \
--cc=procos@jiscmail.ac.uk \
--cc=prog-lang@diku.dk \
--cc=seworld@cs.colorado.edu \
--cc=theory-logic@cs.cmu.edu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox