由买买提看人间百态

boards

本页内容为未名空间相应帖子的节选和存档,一周内的贴子最多显示50字,超过一周显示500字 访问原贴
JobMarket版 - Microsoft-funded PhD opportunity (software/ system verifica
相关主题
有人对EMC职位感兴趣吗 (转载)UK博士招生: Microbiology PHD Student at U of Sheffield
急招 Finance Supervisor (地点:Jersey City, 希望招中国人)Java Engineer / QA Job Opening, San Francisco Bay Area
Ph.D. studentship available at SUNY BinghamtonPost-Doc Position Opening @University of Arizona
Ph.D. studentship available at UNLV2 web dev positions in Redmond, WA
PhD Studentship Available in Wireless Sensor Networks京东北美诚招Senior AI Expert/请联系[email protected]
新加坡管理大学招聘博士后及研究工程师egional Sushi /Hot Food supervisor position
2013 fall- Univerisity of Miami PHD position contact info哪位知道美国的银行怎样进行reference check吗?
德国马普所---博士/博后招聘 (脑功能影像) (转载)半导体猎头/回国机会
相关话题的讨论汇总
话题: microsoft话题: phd话题: project话题: research
进入JobMarket版参与讨论
1 (共1页)
m****s
发帖数: 18160
1
【 以下文字转载自 CS 讨论区 】
发信人: ecfbs (wlec4bs), 信区: CS
标 题: Microsoft-funded PhD opportunity (software/ system verification)
发信站: BBS 未名空间站 (Fri Apr 12 13:40:39 2013, 美东)
Microsoft Research PhD studentship: Future Filesystems
======================================================
Project: Future filesystems: mechanized specification, validation,
implementation and verification of filesystems
Supervisors: Tom Ridge (with Andrew Kennedy at Microsoft Research)
Application deadline: 2013-06-02 (June 2nd)
PhD expected start date: 2013-10-01
We seek strong candidates for a Microsoft PhD studentship on "verified
filesystems". The PhD scholarship is fully funded for three years. The
project will be supervised by Tom Ridge at the Department of Computer
Science, University of Leicester, in collaboration with Andrew Kennedy
at Microsoft Research Cambridge.
Project description
-------------------
Filesystems are extremely important. Users depend on filesystems to
store their files whenever they hit "save". Businesses rely on databases
to store their data safely, and these databases in turn rely on the
filesystem.
Modern filesystems are designed to satisfy many complicated
requirements. As a result, implementations are beset with problems. The
implementation code is extremely complex, and almost inevitably contains
bugs. These bugs can and do lead to data corruption and loss.
Development time is very lengthy. Testing is also very lengthy and
costly, and does not guarantee to eliminate all bugs. It is often
unclear to application developers what guarantees a filesystem provides,
so that it becomes extremely difficult to write correct applications for
a given filesystem, let alone applications that are portable across
different filesystems.
In this project, we aim to tackle these problems by applying formal
methods techniques. We will specify the behaviour of existing
filesystems using higher-order logic (supported by the HOL4 theorem
prover). Further, we will implement a filesystem, and verify functional
correctness of the implementation with respect to the specification. We
are particularly interested in the behaviour of filesystems when the
host crashes. The project involves theoretical aspects (for example, we
are interested in understanding the dependencies that arise when
different filesystem operations execute; the project will also involve
extensive proofs, both informal and mechanized) but is focused on
applications of theory to real-world systems.
Background of applicant
-----------------------
Ideally the applicant should be a good programmer (with knowledge of one
of the main functional programming languages such as OCaml, Haskell, SML
etc), with background in semantics (particularly operational semantics),
theorem proving, and verification. The applicant must have a strong
interest in producing reliable systems.
Applicants should hold at least a good second-class honours degree or
equivalent in computer science (or a closely related discipline) and
have a good command of English. A masters degree may be an advantage,
but is not necessary.
Funding
-------
The Microsoft scholarship consists of an annual bursary for 3 years.
This studentship is fully funded (fees and stipend) for UK and EU
students. The stipend is up to 17,000 UK pounds. We welcome overseas
applicants, and would provide the equivalent of home/EU fees and
maintenance for a successful overseas candidate; the difference between
home/ EU fees and international fees (approx. 11,000 UK pounds per
annum) would need to be funded by the overseas applicant.
Environment
-----------
The Department of Computer Science offers a highly collegiate and
stimulating environment for research career development. The prospective
student will work within an ambitious research team that is
internationally recognised and will be expected to contribute to the
strong profile of the department through participation in the
development and publication of international-quality research results.
Application process
-------------------
We encourage potential applicants who wish to express their interest in
the project to email Tom Ridge `tr61 (at) le.ac.uk` well before the
deadline.
The application process is via the University of Leicester. For further
details on the application process, see
<http://www2.le.ac.uk/study/research/funding/future-filesystems>
Further questions
-----------------
Please contact Tom Ridge `tr61 (at) le.ac.uk` if you have any further
questions.
1 (共1页)
进入JobMarket版参与讨论
相关主题
半导体猎头/回国机会PhD Studentship Available in Wireless Sensor Networks
NE/OK/KS division food supervisor position opening新加坡管理大学招聘博士后及研究工程师
愿意付钱找人推荐工作!2013 fall- Univerisity of Miami PHD position contact info
Production Specialist 这工资,值得去吗德国马普所---博士/博后招聘 (脑功能影像) (转载)
有人对EMC职位感兴趣吗 (转载)UK博士招生: Microbiology PHD Student at U of Sheffield
急招 Finance Supervisor (地点:Jersey City, 希望招中国人)Java Engineer / QA Job Opening, San Francisco Bay Area
Ph.D. studentship available at SUNY BinghamtonPost-Doc Position Opening @University of Arizona
Ph.D. studentship available at UNLV2 web dev positions in Redmond, WA
相关话题的讨论汇总
话题: microsoft话题: phd话题: project话题: research