[TYPES/announce] Postdoc and research engineer positions in Semantics and Verification for Secure Systems Software

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc and research engineer positions in Semantics and Verification for
Secure Systems Software

Advert: http://www.jobs.cam.ac.uk/job/28012/
Closing date: 13 January 2021

Are you interested in developing and applying semantics and verification
techniques to radically improve the foundations and security of mainstream
computer systems? We are looking for postdoctoral researchers and research
assistants to do exactly that, in a wide range of topics.

In recent years, working with Arm, IBM, RISC-V International, the CHERI
team, the C and C++ standards committees, and others, we have shown how one
can develop and use authoritative semantics for full-scale architecture and
language definitions, including instruction-set architectures of ARMv8-A,
RISC-V, and CHERI in our Sail metalanguage (
https://www.cl.cam.ac.uk/~pes20/sail/), our Cerberus C semantics (
https://www.cl.cam.ac.uk/~pes20/cerberus/), and relaxed-memory concurrency
models at the architecture and C/C++ language levels. These use a
combination of semantic definitions made executable as test oracles, test
generation, symbolic execution, and mechanised proof; they have resolved
many questions about what these fundamental abstractions are or should be;
and they can enable both lightweight formal engineering and full
verification of key parts of real systems.

We now aim to build above this in two related projects, for CHERI and Arm
system software.

(1) CHERI verification. CHERI (
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-941.pdf,
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/) extends
conventional hardware Instruction-Set Architectures (ISAs) with new
architectural features, using capabilities, to enable fine-grained memory
protection and highly scalable software compartmentalization. The CHERI
project is led by Robert Watson, Simon Moore, and Peter Sewell at the
University of Cambridge and Peter Neumann at SRI International. CHERI
allows historically memory-unsafe programming languages such as C and C++
to be adapted to protect against many currently widely exploited security
vulnerabilities, and enables the fine-grained decomposition of
operating-system (OS) and application code, to limit the effects of
security vulnerabilities. CHERI is a hardware/software/semantics co-design
project, bringing together computer architecture, systems software,
security, and semantics.

In October 2019, Arm announced Morello (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-morello.html),
an experimental CHERI-extended, multicore, superscalar ARMv8-A processor,
System-on-Chip (SoC), and prototype board. Morello is a part of the UKRI
£187M Digital Security by Design Challenge (DSbD), supported by the UK
Industrial Strategy Challenge Fund, including a commitment of over £50M by
Arm. Morello will support industrial-scale evaluation of CHERI, with a view
to mass-market adoption - which would transform the security landscape.

We have previously developed rigorous engineering methods (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-formal.html)
to precisely define the CHERI ISA, for CHERI-MIPS and CHERI-RISC-V
variants, and to prove (in Isabelle) that they satisfy key intended
security properties (https://www.cl.cam.ac.uk/users/pes20/cheri-formal.pdf).
We are now collaborating with Arm and researchers at the University of
Edinburgh to do the same for the full Morello CHERI ARMv8 ISA, building on
our Sail ARMv8-A ISA semantics, and to study the semantics and security of
higher-level languages and system software above CHERI, building also on
our Cerberus C semantics (https://www.cl.cam.ac.uk/~pes20/cerberus/).
Morello and this verification aim to improve the security of all Arm mobile
device software.

(2) Arm system software verification. This ongoing project, in
collaboration with Google and with researchers at MPI-SWS, Radboud, SNU,
and Aarhus, aims to establish correctness and security properties of key
hypervisor system software above the ARMv8-A ISA semantics mentioned above,
integrated with the ARMv8-A concurrency architecture (including both the
previous "user-mode" models and the system concurrency semantics, being
developed in collaboration with Arm) (
https://www.cl.cam.ac.uk/~pes20/armv8-mca/). The Cambridge work is led by
Peter Sewell, Neel Krishnaswami, and Robert Watson. Here too, there is the
prospect of the resulting system being very widely deployed.

We are looking for postdocs and research assistants to contribute to all
aspects of both projects. You should have a strong background in semantics
and verification, the motivation and flexibility to develop practical ways
to use them at scale for real systems, and experience in one or more of:

- interactive theorem proving, in Coq and/or Isabelle (we use both)
- program logics (especially separation logics and Iris)
- relaxed-memory concurr

[TYPES/announce] semantics/verification postdoc positions at Cambridge

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We're advertising several positions, as below - if you know suitable
candidates, please pass this on. Thanks - Peter


Research Associates/Senior Research Associates in Rigorous Engineering for
Mainstream Systems (Fixed Term), University of Cambridge

Research Associate £32,816 - £40,322 or Senior Research Associate £41,526 -
£52,559

Fixed-term: The funds for these posts are available for 2 years in the
first instance, with a possibility of extension.

Are you interested in developing and applying semantics and verification
techniques to improve the foundations and security of mainstream computer
systems? We are looking for multiple postdoctoral researchers to do exactly
that, in two related projects:

(1) CHERI verification. CHERI (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/) extends
conventional Instruction-Set Architectures (ISAs) with architectural
capabilities, for fine-grained memory protection and scalable software
compartmentalization. CHERI allows memory-unsafe programming languages, eg
C and C++, to be adapted to protect against many currently widely exploited
security vulnerabilities. CHERI is a hardware/software/semantics co-design
project, combining computer architecture, systems software, security, and
semantics.

In October 2019, Arm announced Morello (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-morello.html),
an experimental CHERI-extended ARMv8-A processor, to be available from late
2021. Morello is part of the UKRI £187M Digital Security by Design
Challenge (DSbD), supported by the UK Industrial Strategy Challenge Fund
and over £50M from Arm. Morello will support industrial-scale evaluation of
CHERI, with a view to mass-market adoption - which would transform the
security landscape.

We have previously developed rigorous engineering methods (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-formal.html)
to precisely define the CHERI ISA, for CHERI-MIPS and CHERI-RISC-V
variants, and to prove (in Isabelle) that they satisfy key intended
security properties (https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-940.pdf
).

We are now collaborating with Arm and researchers at Edinburgh to do the
same for the full Morello CHERI ARMv8 ISA, building on our Sail ARMv8-A ISA
semantics (https://www.cl.cam.ac.uk/~pes20/sail/), and to study the
semantics and security of higher-level languages and system software above
CHERI, building on our Cerberus C semantics (
https://www.cl.cam.ac.uk/~pes20/cerberus/). This verification could improve
the security of all Arm mobile device software.

(2) Arm system software verification. We have an ongoing project, in
collaboration with Google and with researchers at multiple institutions, to
establish correctness and security properties of key system software above
the ARMv8-A ISA semantics (https://www.cl.cam.ac.uk/~pes20/sail/),
integrated with the ARMv8-A concurrency architecture (including both the
previous "user-mode" models and the system concurrency semantics, being
developed in collaboration with Arm) (
https://www.cl.cam.ac.uk/~pes20/armv8-mca/).

We are looking for postdocs to contribute to all aspects of both projects.
You should have a strong background in semantics and verification, the
motivation and flexibility to develop practical ways to use them at scale
for real systems, and experience in one or more of:

- interactive theorem proving, in Coq, HOL4, and/or Isabelle
- program logics
- low-level system software
- programming language semantics and type systems
- program analysis
- hardware verification
- functional programming

We are also seeking candidates with a research engineering focus, to assist
in the development of robust and widely usable tools based on the above.
For this, you should have experience in functional programming, especially
OCaml.

There might also be the possibility of internship or PhD positions; for
these contact Prof. Sewell.

For more details of our recent work, see (https://www.cl.cam.ac.uk/~pes20/),
and especially REMS (https://www.cl.cam.ac.uk/~pes20/rems/index.html).

The positions are available to start as soon as possible. For candidates
with substantial relevant expertise, we may be able to appoint at the
Senior Research Associate level.

Further details may be obtained from Prof. Peter Sewell,
peter.sew...@cl.cam.ac.uk

Click the 'Apply' button at (http://www.jobs.cam.ac.uk/job/24501/) to apply
online.

You will need to upload a full curriculum vitae (CV) and a covering letter
outlining your interests, potential contributions, and relevant past
experience; you should also include the contact details for at least 2
referees.

Please quote reference NR21859 on your application and in any
correspondence about this vacancy.

The University actively supports equality, diversity and inclusion and
encourages applications from all sections of society.

The Univ

[TYPES/announce] Faculty position in PL at U. Cambridge

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

 We're advertising a faculty position in Programming Languages (considered
broadly) at Cambridge:


http://www.jobs.cam.ac.uk/job/21863/

The Department of Computer Science and Technology, also known as the
University of Cambridge Computer Laboratory, is seeking to recruit a new
faculty member at the Lecturer or Senior Lecturer level (analogous to a US
Associate Professor) who can contribute to research and teaching in the
broad area of Programming Languages. This includes (but is not limited to)
Compilation, Program Analysis, Program Transformation, Type Systems,
Semantics, Verification, Security, and Concurrency.

The ideal candidate will have interests ranging from practical applications
to their underlying semantic theory, with the potential to form new
collaborations with Departmental staff across a range of topics, e.g. in
Security, Operating Systems, Computer Architecture, and/or Networking.

Notwithstanding the above focus, in exceptional cases we may appoint in any
area of Computer Science.

It is likely that successful candidates will already have a strong track
record in one or more relevant research areas and already have some
postdoctoral experience. Ideally the candidate will also have experience of
teaching and of generating research grant income.

Please pass this on to any likely candidates.

thanks,

Peter

Re: [TYPES/announce] Postdoc position in Applied Semantics for Production Architectures

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

On 15 December 2016 at 23:20, Peter Sewell <peter.sew...@cl.cam.ac.uk>
wrote:

> [please circulate this to any likely candidates - thanks, Peter]
>
> Research Associate/Senior Research Associate in Applied Semantics for
> Production Architectures
>

Updating this: the likellihood of new funding means we may be able to make
several appointments, to build a really strong team.   Closing date 24 Jan,
as before.

Peter



> University of Cambridge Computer Laboratory
> Research Associate £29,301 - £38,183 or Senior Research Associate £39,324
> - 49,772
> Fixed-term: until February 28, 2019, when the grant funding the post
> currently ends.
> Details: http://www.jobs.cam.ac.uk/job/12397/
>
>
> Do you want to help build mathematically rigorous foundations for
> real-world computing, to make it more robust and secure?
>
> We have an ongoing project to establish rigorous semantic models for
> production multiprocessors, to provide a clear basis for programming,
> software verification, and hardware verification. This involves long-term
> close collaborations with ARM and IBM, and we have an agreement with ARM to
> take their internal ISA description, build a mathematical model based on
> it, integrate it with the concurrency semantics we are developing, and
> release the whole in a form usable for verification. This will provide the
> first strongly validated public model for a production multiprocessor
> architecture. We also have a close collaboration with the CHERI research
> project, developing processors with hardware-accelerated in-process memory
> protection and sandboxing, together with an open-source operating system
> and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the
> heart of the CHERI design process. For more details, see some of our
> previous papers:
> POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (
> http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (
> http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (
> http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf),
> CHERI ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html),
> CHERI (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (
> http://rems.io).
>
> We have a position available to work on:
>
> - the development of our Sail metalanguage for ISA description: a language
> with a lightweight dependent type system, designed to capture ARM, IBM
> POWER, and CHERI instruction semantics in an engineer-friendly way;
> - translation from Sail to generate efficient emulators and usable
> theorem-prover definitions;
> - mechanised proof about the architecture definitions, e.g. of security
> properties, relationships between concurrency models, and correctness
> results for high-level language concurrency compilation; and/or
> - development of reasoning, symbolic execution, debugging, and/or
> model-checking tools above the architecture definitions - the initial work
> should generate many opportunities along these lines.
>
> The successful candidate must have a PhD (or equivalent experience), a
> track-record of publication in relevant areas of Computer Science, good
> knowledge of English and communication skills, and the expertise and
> commitment to apply rigorous semantics to real systems. We're looking for
> people with the skills to make solid models and tools, well-engineered and
> widely usable. You should have expertise in one or more of:
>
> - functional programming (e.g. OCaml)
> - programming language semantics and type systems
> - theorem provers, especially Isabelle and/or Coq
> - symbolic execution
> - model-checking
>
> For senior applicants, e.g. who will be able to contribute substantially
> to future grant applications, it may be possible to appoint at the Senior
> Research Associate level.
>
> This is part of the broader REMS (Rigorous Engineering for Mainstream
> Systems) programme grant: a lively collaboration between systems and
> semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and
> apply mathematically rigorous semantics to mainstream systems.
>
> Informal enquiries should be directed to Peter Sewell (
> peter.sew...@cl.cam.ac.uk).
>
> To apply online for this vacancy, please click on the 'Apply' button
> below. This will route you to the University's Web Recruitment System,
> where you will need to register an account (if you have not already) and
> log in before completing the online application form.
>
> Please ensure you upload your Curriculum Vitae (CV) and a cover letter
> explaining your potential contribution to the project, 

[TYPES/announce] Postdoc position in Applied Semantics for Production Architectures

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

[please circulate this to any likely candidates - thanks, Peter]

Research Associate/Senior Research Associate in Applied Semantics for
Production Architectures

University of Cambridge Computer Laboratory
Research Associate £29,301 - £38,183 or Senior Research Associate £39,324 -
49,772
Fixed-term: until February 28, 2019, when the grant funding the post
currently ends.
Details: http://www.jobs.cam.ac.uk/job/12397/


Do you want to help build mathematically rigorous foundations for
real-world computing, to make it more robust and secure?

We have an ongoing project to establish rigorous semantic models for
production multiprocessors, to provide a clear basis for programming,
software verification, and hardware verification. This involves long-term
close collaborations with ARM and IBM, and we have an agreement with ARM to
take their internal ISA description, build a mathematical model based on
it, integrate it with the concurrency semantics we are developing, and
release the whole in a form usable for verification. This will provide the
first strongly validated public model for a production multiprocessor
architecture. We also have a close collaboration with the CHERI research
project, developing processors with hardware-accelerated in-process memory
protection and sandboxing, together with an open-source operating system
and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the
heart of the CHERI design process. For more details, see some of our
previous papers:
POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (
http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (
http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (
http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf), CHERI
ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html), CHERI (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (
http://rems.io).

We have a position available to work on:

- the development of our Sail metalanguage for ISA description: a language
with a lightweight dependent type system, designed to capture ARM, IBM
POWER, and CHERI instruction semantics in an engineer-friendly way;
- translation from Sail to generate efficient emulators and usable
theorem-prover definitions;
- mechanised proof about the architecture definitions, e.g. of security
properties, relationships between concurrency models, and correctness
results for high-level language concurrency compilation; and/or
- development of reasoning, symbolic execution, debugging, and/or
model-checking tools above the architecture definitions - the initial work
should generate many opportunities along these lines.

The successful candidate must have a PhD (or equivalent experience), a
track-record of publication in relevant areas of Computer Science, good
knowledge of English and communication skills, and the expertise and
commitment to apply rigorous semantics to real systems. We're looking for
people with the skills to make solid models and tools, well-engineered and
widely usable. You should have expertise in one or more of:

- functional programming (e.g. OCaml)
- programming language semantics and type systems
- theorem provers, especially Isabelle and/or Coq
- symbolic execution
- model-checking

For senior applicants, e.g. who will be able to contribute substantially to
future grant applications, it may be possible to appoint at the Senior
Research Associate level.

This is part of the broader REMS (Rigorous Engineering for Mainstream
Systems) programme grant: a lively collaboration between systems and
semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and
apply mathematically rigorous semantics to mainstream systems.

Informal enquiries should be directed to Peter Sewell (
peter.sew...@cl.cam.ac.uk).

To apply online for this vacancy, please click on the 'Apply' button below.
This will route you to the University's Web Recruitment System, where you
will need to register an account (if you have not already) and log in
before completing the online application form.

Please ensure you upload your Curriculum Vitae (CV) and a cover letter
explaining your potential contribution to the project, as pdf documents.
Include the names of 2 or 3 referees at the appropriate point in the online
application. Your referees should be prepared to send references within a
week of the closing date, if asked by the University. If you upload any
additional documents which have not been requested, we will not be able to
consider these as part of your application.

Please quote reference NR10978 on your application and in any
correspondence about this vacancy.

The University values diversity and is committed to equality of opportunity.

The University has a responsibility to ensure that all employees are
eligible to live and work in the UK.

[TYPES/announce] PiP 2017: Principles in Practice - Call for Participation

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

PiP 2017: Principles in Practice

Co-located with POPL 2017 <http://popl17.sigplan.org>

Saturday 21st January, 2017. Paris, France

Recent years have seen a number of research projects applying rigorous
semantics to the analysis or design of industrially significant real-world
languages and systems, in various contexts. Principles in Practice (PiP) is
an informal workshop bringing together researchers to discuss the issues
involved in engaging with the various industrial communities, in developing
and using semantics at scale, in handling pre-existing systems complexity,
and in the wide range of testing, analysis, and proof-based techniques that
can be applied. There is a programme of invited talks, with no proceedings.

This follows the previous PiP 2014
<http://www.cl.cam.ac.uk/%7Epes20/pip2014.html> workshop.
Registration Registration is via the POPL 2017 <http://popl17.sigplan.org>
registration page. Preliminary Schedule

   - 08:55 Welcome
   - 09:00-10:00
  - 09:00-09:30 * Andrew Kennedy* (Facebook) Static type checking for
  PHP
  - 09:30-10:00 * Jean-Louis Colaco * (Ansys) Scade
   - 10:00-10:30 coffee break
   - 10:30-12:05 REMS session
      - 10:30-10:35 *Peter Sewell* (Cambridge) REMS Short Introduction
  - 10:35-11:05 *Simon Moore* (Cambridge) Experiences of Formal
  Modelling in the CHERI Computer Architecture Research Project
  - 11:05-11:35 * Stephen Kell/Dominic Mulligan* (Cambridge) ELF
  linking: what it means and why it matters
  - 11:35-12:05* Philippa Gardner* (Imperial) Towards Tractable
  Verification of JavaScript Programs
   - 12:05-14:00 lunch
   - 14:00-15:30
  - 14:00-14:30 * John Hughes* (Quviq/Chalmers) Properties in practice:
  lessons from ten years of QuickCheck
  - 14:30-15:00 * Byron Cook* (Amazon) Automated Reasoning about AWS
  - 15:00-15:30 * Steve Zdancewic* (U.Penn) Vellvm2: Semantics and
  Verification for LLVM
   15:30-16:00 coffee break
   - 16:00-17:30
  - 16:00-16:30 *Christopher Pulte/Kathryn Gray* (Cambridge) REMS
  machine models
  - 16:30-17:30 *Discussion session* Methods and Tools for large-scale
  semantics

[TYPES/announce] Fwd: Faculty position in PL/verification/theorem proving at Cambridge

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

[Deadline 17th January]

-- Forwarded message --
Subject: Faculty position in PL/verification/theorem proving at Cambridge
To: types-announce@lists.seas.upenn.edu


http://www.jobs.cam.ac.uk/job/8134/

[this is roughly analogous to a US tenured associate professor position]

The University of Cambridge Computer Laboratory is seeking to recruit
a new faculty member at the Lecturer or Senior Lecturer level who can
contribute to research in areas such as (but not limited to) the
following:

theoretical foundations of programming
programming language design and implementation
formal specification and verification of computer systems
theorem proving and its application to hardware and software

The ideal candidate will have interests that range from mathematical
theory to practical applications and will demonstrate the potential to
collaborate with Computer Laboratory research students, staff and
faculty across a range of topics.

Notwithstanding the above focus, exceptional candidates from any area
of Computer Science are also encouraged to apply.

It is likely that successful candidates will already have a strong
track record in one or more relevant research areas and already have
some postdoctoral experience. Ideally the candidate will also have
experience of teaching and generating research grant income.

[TYPES/announce] Faculty position in PL/verification/theorem proving at Cambridge

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

http://www.jobs.cam.ac.uk/job/8134/

[this is roughly analogous to a US tenured associate professor position]

The University of Cambridge Computer Laboratory is seeking to recruit
a new faculty member at the Lecturer or Senior Lecturer level who can
contribute to research in areas such as (but not limited to) the
following:

theoretical foundations of programming
programming language design and implementation
formal specification and verification of computer systems
theorem proving and its application to hardware and software

The ideal candidate will have interests that range from mathematical
theory to practical applications and will demonstrate the potential to
collaborate with Computer Laboratory research students, staff and
faculty across a range of topics.

Notwithstanding the above focus, exceptional candidates from any area
of Computer Science are also encouraged to apply.

It is likely that successful candidates will already have a strong
track record in one or more relevant research areas and already have
some postdoctoral experience. Ideally the candidate will also have
experience of teaching and generating research grant income.

[TYPES/announce] REMS postdoc researcher / research-engineer positions

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,

we've just advertised for two postdoc researcher / research-engineer
positions, to work with the REMS semantic models of key
infrastructure interfaces (multiprocessor semantics, C, ELF,
filesystems, TCP, TLS ...), emulators and verification tools built
above those, and the semantic tools we use to express them (Lem, Ott,
Coq, HOL4, Isabelle/HOL). If you know of any good potential
candidates, please draw this to their attention:

http://www.jobs.cam.ac.uk/job/7576/

thanks,
Peter

[TYPES/announce] Call for Participation: Principles in Practice 2014 (co-located with POPL)

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

PiP 2014: Principles in Practice

Co-located with POPL 2014
Saturday 25 January, 2014. San Diego, California, USA
http://www.cl.cam.ac.uk/~pes20/pip2014.html

Recent years have seen a number research projects applying rigorous
semantics to the analysis or design of industrially significant
real-world languages and systems, in various contexts. Principles in
Practice (PiP) is an informal workshop bringing together researchers
to discuss the issues involved in engaging with the various industrial
communities, in developing and using semantics at scale, in handling
pre-existing systems complexity, and in the wide range of testing,
analysis, and proof-based techniques that can be applied. There will
be a programme of invited talks, with no proceedings.


Speakers

* Peter Sewell, Introduction and REMS project (10 minutes)

* Andrew Kennedy / Nick Benton, Formalizing .EXEs, .DLLs, and all that

* Benjamin Pierce, Verification and random testing of the SAFE architecture

* Daniel Kroening, Automated test-suite generation for automotive applications

* Gang Tan / Greg Morrisett, Reusable tools for formal modeling of machine code

* Konrad Slind (Rockwell Collins), Industrial verification considered
as a helix of semi-precious stones

* Michael Norrish, Ad hoc C: reflections on pragmatic semantics

* Sergio Maffeis, Formal, executable semantics of web languages:
JavaScript and PHP

* Shriram Krishnamurthi, Programming Language Semantics as Natural
Science: The Peculiar, Evolving, and Barely Consummated Relationship
Between Semantics and Scripting Languages

* Xavier Leroy, How much is a mechanized proof worth, certification-wise?

* Zhong Shao, Advanced Development of Certified OS Kernels

Registration is via the POPL 2014 registration page. PiP 2014 is not
an ACM-sponsored meeting, so if you plan to attend, please register
specifically for PiP. Breakfast and breaks will be included, but not
lunch.

Organisers

Peter Sewell, University of Cambridge, UK
Steve Zdancewic, University of Pennsylvania, USA

Sponsors

PiP 2014 is sponsored by the EPSRC REMS project: Rigorous Engineering
for Mainstream Systems.

[TYPES/announce] Post-Doc and PhD positions - Semantics of Real-World Computer Systems

[Peter Sewell]

[ The Types Forum (announcements only), 
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]



[Please bring these to the attention of any suitably qualified
candidates - thanks, Peter]


*

Research Associate
University of Cambridge - Faculty of Computer Science  Technology

Salary: £27,319 - £35,646 pa

Limit of tenure: Up to 2 years

We are seeking a Post-Doctoral Research Associate to join a lively
group working on the semantics of real-world computer systems, with a
focus on the relaxed-memory concurrency they exhibit.  Current
projects include work on the memory models of multiprocessors (x86,
Power, ARM) and of programming languages (C++0X/C1X, Java), verified
compilation of concurrent programming languages to multiprocessors,
the semantic theory of relaxed-memory concurrency, and the development
of tool support for semantics.

You should have a keen interest in applying rigorous semantic
techniques to real-world systems, with a strong background in one or
more of the following:

* Programming Language Semantics
* Automated Proof Assistants
* Relaxed Memory Models
* Program Verification

The position is funded by the EPRSC grant EP/H005633,
http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/H005633/1, led by
Peter Sewell (http://www.cl.cam.ac.uk/~pes20/), to whom enquiries
should be addressed.

Applications should include:

* a Curriculum Vitae
* a brief statement of the particular contribution you would make
to the project
* a completed form CHRIS6:
  http://www.admin.cam.ac.uk/offices/hr/forms/chris6/
* the names and contact details (postal and e-mail addresses) of
two or three referees.

Start date: as soon as possible after 4th October 2010

Complete applications should be sent by post to: Personnel-Admin,
University of Cambridge, Computer Laboratory, 15 JJ Thomson Avenue,
Cambridge CB3 0FD, United Kingdom, or by e-mail to
personnel-ad...@cl.cam.ac.uk.

Quote Reference: NR07133, Closing Date: 4 October 2010

The University values diversity and is committed to equality of
opportunity.


*

PhD Studentships
University of Cambridge - Faculty of Computer Science  Technology

We are seeking two PhD students to join a lively group working on the
semantics of real-world computer systems, with a focus on the
relaxed-memory concurrency they exhibit.  Current projects include
work on the memory models of multiprocessors (x86, Power, ARM) and of
programming languages (C++0X/C1X, Java), verified compilation of
concurrent programming languages to multiprocessors, the semantic
theory of relaxed-memory concurrency, and the development of tool
support for semantics.

You should have a keen interest in applying mathematically rigorous
semantic techniques to real-world systems, ideally with experience in
one or more of the following:

* Programming Language Semantics
* Automated Proof Assistants
* Relaxed Memory Models
* Program Verification

Informal enquiries should be addressed to Peter Sewell
(http://www.cl.cam.ac.uk/~pes20/), including a Curriculum Vitae and a
brief statement of your background and interests.

The positions are funded by the EPRSC grant EP/H005633,
http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/H005633/1.

For UK/EU students this covers a stipend and fees.  For October 2011
entry, applications should ideally be received by December 1 2010
(applications for earlier start dates may also be considered).

Non-UK/EU students will require additional funding for the higher
level of fees. Exceptional non-EU candidates may be considered for
nomination to the Gates Cambridge Trust and Cambridge International
Scholarship competitions.  The application deadline (for October 2011
entry) for these is October 15 2010 for US applicants and December 1
for non-US applicants (note that applications must be complete by
these deadlines, including transcripts, references, degree
certificates, and research proposal).

More information on the formal application process is here:
http://www.cl.cam.ac.uk/admissions/phd/.

Quote Reference: NR07135.

The University values diversity and is committed to equality of
opportunity.



*