[TYPES/announce] Rust Verification Workshop at ETAPS 2023: Call for Talk and Demo Proposals

[Mueller Peter]

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

Call for Talk and Demo Proposals
3rd Rust Verification Workshop
Co-located with ETAPS 2023
Paris, France
Sunday, April 23, 2023
https://urldefense.com/v3/__https://sites.google.com/view/rustverify2023/home__;!!IBzWLUs!WvjSkEvaJwWW-00m5MDND8mwv4QX1kSLQH1NoxnBuQo9q_U90qHogB_iZu2NLX8yIy9kr0w7Kov1S_ft7QaeenmG23DeZb42ewX9IBtfTAI$
 

Rust is a recently introduced programming language for writing performant code 
with strong type and memory safety guarantees. It is considered a serious 
alternative to C and C++ for systems programming, because it provides 
high-level abstractions but without the cost of garbage collection. Given the 
growing popularity of Rust, and given that bugs in systems programs can be 
costly, there is growing interest in the program verification community for 
building program verifiers for Rust. In this workshop, we aim to bring together 
language designers, application developers and formal verification tool 
builders, to exchange ideas and build collaborations around developing verified 
Rust programs.
The goal of this workshop is to bring researchers from a variety of different 
backgrounds and perspectives together to exchange new and exciting ideas 
concerning the verification of Rust programs and exploring avenues for 
collaboration.
We want the workshop to be as informal and interactive as possible. The program 
will thus involve a combination of invited talks, contributed talks about work 
in progress, tool demos, and open discussion sessions. There will be no 
published proceedings, but participants will be invited to submit working 
documents, talk slides, etc. to be posted on this website.

Call for Talk and Demo Proposals
-
We solicit proposals for contributed talks and tool demos. Proposals should be 
at most 2 pages, in either plain text or PDF format, and should specify how 
long a talk/demo the speaker wishes to give. By default, contributed talks will 
be 30 minutes long, but proposals for shorter or longer talks will also be 
considered.
We are interested in talks/demos on all topics related to the verification of 
Rust programs (including, for instance, program specification, deductive 
verification, model checking, symbolic execution, runtime monitoring, the 
semantics and formalization of Rust, and tool support). Talks about work in 
progress as well as proposals for challenge problems in Rust are particularly 
encouraged.
Please submit by email to 
peter.muel...@inf.ethz.ch.

Important Dates
-
Deadline for talk/demo proposals:January 20, 2023 (Friday)
Notification of acceptance:February 10, 2023 (Friday)
Workshop: April 23, 2023 (Sunday)

Organizers

Rajeev Joshi, Amazon Web Services 
mailto:joraj...@amazon.com>>
Nicholas Matsakis, Amazon Web Services 
Peter Müller, ETH Zurich 

[TYPES/announce] Rust Verification Workshop at ETAPS 2022: Call for Talk and Demo Proposals

[Mueller Peter]

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

Call for Talk, Demo, and Challenge Proposals
2nd Rust Verification Workshop
Co-located with ETAPS 2022
Munich
Sunday, April 03, 2022
https://urldefense.com/v3/__https://sites.google.com/view/rustverify2022/home__;!!IBzWLUs!G4xwjmn6v93mHpZ6Tt37BnYL14gdxWDDKZgSwlO-9Sfrs9hqogM9RNBGcF9FAYII5X9yrr7wYQZqUg$
 

Rust is a new programming language for writing performant code with strong type 
and memory safety guarantees. It is now considered a serious alternative to C 
and C++ for systems programming, because it provides high-level abstractions 
but without the cost of garbage collection. Given the growing popularity of 
Rust, and given that bugs in systems programs can be costly, there is growing 
interest in the program verification community for building program verifiers 
for Rust. In this workshop, we aim to bring together language designers, 
application developers and formal verification tool builders, to exchange ideas 
and build collaborations around developing verified Rust programs.
The goal of this workshop is to bring researchers from a variety of different 
backgrounds and perspectives together to exchange new and exciting ideas 
concerning the verification of Rust programs and exploring avenues for 
collaboration.
We want the workshop to be as informal and interactive as possible. The program 
will thus involve a combination of invited talks, contributed talks about work 
in progress, tool demos, and open discussion sessions. There will be no 
published proceedings, but participants will be invited to submit working 
documents, talk slides, etc. to be posted on this website.

Call for Talk and Demo Proposals
-
We solicit proposals for contributed talks and tool demos. Proposals should be 
at most 2 pages, in either plain text or PDF format, and should specify how 
long a talk/demo the speaker wishes to give. By default, contributed talks will 
be 30 minutes long, but proposals for shorter or longer talks will also be 
considered.
We are interested in talks/demos on all topics related to the verification of 
Rust programs (including, for instance, program specification, deductive 
verification, model checking, symbolic execution, runtime monitoring, the 
semantics and formalization of Rust, and tool support). Talks about work in 
progress as well as proposals for challenge problems in Rust are particularly 
encouraged.
Please submit by email to 
peter.muel...@inf.ethz.ch.

Important Dates
-
Deadline for talk/demo proposals:January 14, 2022 (Friday)
Notification of acceptance: February 07, 2022 (Monday)
Workshop:   April 03, 2022 (Sunday)

Organizers

Rajeev Joshi, Amazon Web Services 
mailto:joraj...@amazon.com>>
Nicholas Matsakis, Mozilla mailto:nmatsa...@mozilla.com>>
Peter Müller, ETH Zurich 

[TYPES/announce] PhD student and post-doc positions in Program Verification at ETH Zurich

[Mueller Peter]

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

The Programming Methodology group (http://www.pm.inf.ethz.ch/) at ETH Zurich is 
recruiting PhD students and post-docs in the area of program verification. We 
are especially interested in strengthening our teams working on Rust 
verification (https://www.pm.inf.ethz.ch/research/prusti.html) and Go 
verification (https://www.pm.inf.ethz.ch/research/gobra.html). Our goal is to 
develop verification techniques and tools that can be used to prove correctness 
and security of advanced systems.
Key requirements for successful applications:
* Strong commitment to research
* Interest in combining theory and practice
* For PhD students: excellent M.Sc. degree in Computer Science or in a related 
subject with a strong Computer Science component
* For post-docs: publications in top conferences or journals
* Proficiency in English and excellent communication skills, both oral and 
written
Applications and questions should be sent to Peter Müller 
(jobs...@inf.ethz.ch). The application should 
include a CV and a description of research interests. We will consider 
applications until the positions are filled. The start date is negotiable.
More details about the positions:
* PhD and post-doc positions are fully funded and have an attractive salary and 
social benefits.
* Full scholarships are available for outstanding B.Sc. students interested in 
the PhD.
* ETH has one of the top computer science departments in the world
* Zurich is consistently ranked among the top destinations in the world for 
quality of life.
General information on doctoral studies at ETH is available at 
www.inf.ethz.ch/doctorate.html

[TYPES/announce] Call for participation: 1st Rust Verification Workshop

[Mueller Peter]

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

1st Rust Verification Workshop
Online, co-located with ETAPS 2021
April 07, 09, and 12, 2021, 16:00 - 18:10 GMT
https://sites.google.com/view/rustverify2021

Rust is a new programming language for writing performant code with strong type 
and memory safety guarantees. It is now considered a serious alternative to C 
and C++ for systems programming, because it provides high-level abstractions 
but without the cost of garbage collection. Given the growing popularity of 
Rust, and given that bugs in systems programs can be costly, there is growing 
interest in the program verification community for building program verifiers 
for Rust. In this workshop, we aim to bring together language designers, 
application developers and formal verification tool builders, to exchange ideas 
and build collaborations around developing verified Rust programs.
The goal of this workshop is to bring researchers from a variety of different 
backgrounds and perspectives together to exchange new and exciting ideas 
concerning the verification of Rust programs and exploring avenues for 
collaboration.
The program will contains a combination of invited talks and contributed talks. 
A detailed schedule is available here: 
https://sites.google.com/view/rustverify2021.

Registration
Please register via ETAPS at https://etaps.org/2021/registration. You will 
receive access information once you have registered.


Organizers:

  *   Rajeev Joshi, Amazon Web Services
  *   Nicholas Matsakis, Amazon Web Services
  *   Peter Müller, ETH Zurich

[TYPES/announce] Rust Verification Workshop at ETAPS 2021: Call for Talk and Demo Proposals

[Mueller Peter]

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

Call for Talk and Demo Proposals
1st Rust Verification Workshop
Co-located with ETAPS 2021
Luxembourg
Sunday, 28 March, 2021
https://sites.google.com/view/rustverify2021

Rust is a new programming language for writing performant code with strong type 
and memory safety guarantees. It is now considered a serious alternative to C 
and C++ for systems programming, because it provides high-level abstractions 
but without the cost of garbage collection. Given the growing popularity of 
Rust, and given that bugs in systems programs can be costly, there is growing 
interest in the program verification community for building program verifiers 
for Rust. In this workshop, we aim to bring together language designers, 
application developers and formal verification tool builders, to exchange ideas 
and build collaborations around developing verified Rust programs.
The goal of this workshop is to bring researchers from a variety of different 
backgrounds and perspectives together to exchange new and exciting ideas 
concerning the verification of Rust programs and exploring avenues for 
collaboration.
We want the workshop to be as informal and interactive as possible. The program 
will thus involve a combination of invited talks, contributed talks about work 
in progress, tool demos, and open-ended discussion sessions. There will be no 
published proceedings, but participants will be invited to submit working 
documents, talk slides, etc. to be posted on this website.

Call for Talk and Demo Proposals
We solicit proposals for contributed talks and tool demos. Proposals should be 
at most 2 pages, in either plain text or PDF format, and should specify how 
long a talk/demo the speaker wishes to give. By default, contributed talks will 
be 30 minutes long, but proposals for shorter or longer talks will also be 
considered.
We are interested in talks/demos on all topics related to the verification of 
Rust programs (including, for instance, program specification, deductive 
verification, model checking, symbolic execution, runtime monitoring, the 
semantics and formalization of Rust, and tool support). Talks about work in 
progress as well as proposals for challenge problems in Rust are particularly 
encouraged.

Please submit proposals by email to 
peter.muel...@inf.ethz.ch.

Important Dates:
§ 15 January, 2021: Abstract Submission Deadline
§ 25 January, 2021: Notification of Acceptance
§ 28 March, 2021: Workshop
Note: In the event that ETAPS is held virtually, the workshop will be held 
virtually as well.  We'll update the web site as we learn more.

Workshop web site: https://sites.google.com/view/rustverify2021

Organizers:

  *   Rajeev Joshi, Amazon Web Services 
mailto:joraj...@amazon.com>>
  *   Nicholas Matsakis, Mozilla 
nmatsa...@mozilla.com
  *   Peter Müller, ETH Zurich 
mailto:peter.muel...@inf.ethz.ch>>

[TYPES/announce] MARKTOBERDORF SUMMER SCHOOL 2020: CALL FOR PARTICIPATION

[Mueller Peter]

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

CALL FOR PARTICIPATION


MARKTOBERDORF INTERNATIONAL SUMMER SCHOOL ON ENGINEERING SECURE AND DEPENDABLE 
SOFTWARE SYSTEMS
July 29th-August 7th, 2020, Marktoberdorf, Germany
http://marktoberdorf.fortiss.org

Sponsored by Amazon Web Services, https://aws.amazon.com/de/
Organized by fortiss, https://www.fortiss.org/en/

APPLY ONLINE ON OR BEFORE APRIL 19th:
https://i4.pages.gitlab.lrz.de/organization/mod-2020/participation


*** Lectures, see https://i4.pages.gitlab.lrz.de/organization/mod-2020/lectures 
***
Marsha Chechik, University of Toronto: tba
Mike Dodds, Galois, Inc.: Formal methods at scale
Cédric Fournet, Microsoft Research: tba
Xiaowei Huang, University of Liverpool: Safety Certification of Deep Neural 
Networks
Guy Katz, Hebrew University of Jerusalem: Formal Verification of Deep 
Neural Networks
Rustan Leino, Amazon Web Services: Program Proofs
Peter Müller (co-director), ETH Zurich: Verification of Rust Programs - 
Reasoning about Imperative Programs using Ownership
Frank Piessens, KU Leuven: Software security: cross-layer attacks and 
defenses
Alexander Pretschner (co-director), TU München and fortiss: Testing 
Autonomous Cars
Cesare Tinelli, University of Iowa: Theory and practice of Satisfiability 
Modulo Theories


*** Objective: ***
Almost all modern technical systems rely crucially on software.
Communication, transportation, financial services, healthcare, power supply, 
military defense, and many other aspects of modern societies require software 
systems that are both safe and secure. Safe software behaves according to its 
specification and, in particular, avoids hazards for the environment it is used 
in. Secure software ensures the confidentiality, integrity, and availability of 
data, even when a system is attacked by an adversary. Both safety and security 
violations potentially cause considerable economic, political, and physical 
damage. So, improving our understanding of safety and security and, thereby, 
enhancing our ability to construct safe and secure systems is a vital challenge 
for our society.

The lectures in this summer school give an overview of the state of the art in 
the construction and analysis of safe and secure systems. Starting from the 
logical and semantic foundations that enable reasoning about classical software 
systems, they extend to the development and verification of cyber-physical 
systems, which tightly combine computational and physical components, and have 
become pervasive in aerospace, automotive, industry automation, and consumer 
appliances. Safety and security have traditionally been considered separate; 
however, several lectures in this summer school will emphasize their 
commonalities and present analysis and construction techniques that apply to 
both.


*** Marktoberdorf Summer School ***
As a follow-up to the famous 1968 conference in Garmisch-Partenkirchen, 
Professor F.L. Bauer from the Technical University of Munich co-organized the 
first Marktoberdorf Summer School in 1970. We are happy to announce the 41st 
edition of the most prestigious summer school on software engineering in 2020.

[TYPES/announce] Senior Postdoc / Project Coordinator position in Information Security and Program Verification at ETH Zurich

[Mueller Peter]

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

Senior Postdoc / Project Coordinator position in Information Security and 
Program Verification at ETH Zurich

The Institute of Information Security (the groups of Prof. Adrian Perrig and 
Prof. David Basin) and the Programming Methodology Group (Prof. Peter Müller) 
at ETH Zurich are hiring a Postdoc in a large research project in the area of 
digital trust. The goal of this project is to develop a comprehensive, formally 
verified security architecture for communication in the physical and digital 
world. In particular, the project will develop protocols to transfer physical 
trust relationships into the digital world and store, manage, and use them. The 
design will take into account human (mis-)behavior from the outset. A 
particular emphasis is on the formal verification of the architecture both at 
the design and implementation level to rule out any undesired behavior.

We are looking for enthusiastic and outstanding postdoctoral researchers with a 
strong background in some of the following topics:

  *   formal modeling and verification,
  *   program verification,
  *   theorem proving, model checking,
  *   cryptographic protocols,
  *   public-key infrastructure, identity management, authentication,
  *   networking and distributed systems, and
  *   design and implementation of security architectures.

In addition to research, the responsibilities of the position include project 
management, in particular, coordination among the involved research groups, 
lightweight reporting to the funding agency, and outreach to potential 
industrial users of the developed solutions.

All candidates matching the profile above are encouraged to apply as soon as 
possible. We will process applications until all positions are filled. 
Successful candidates are expected to start soon after acceptance, but the 
starting date is negotiable.

Applications should include:

  *   a curriculum vitae,
  *   a brief description of research interests, and
  *   letters of recommendation.

Applications and inquiries should be sent to Christoph Sprenger and Sandra 
Schneider at the following email addresses.

  infsec.positi...@inf.ethz.ch, 
jobs...@inf.ethz.ch
Postdocs are paid employees of ETH Zurich. Salary and employment conditions are 
attractive. Zurich is a diverse and multicultural city which is consistently 
rated among the best cities in the world in which to live.

[TYPES/announce] Rust Verification Workshop at ETAPS 2020: Call for Talk, Demo, and Challenge Proposals

[Mueller Peter]

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

Call for Talk, Demo, and Challenge Proposals
1st Rust Verification Workshop

Co-located with ETAPS 2020
Dublin, Ireland
Sunday, 26 April, 2020
https://sites.google.com/view/rustverify2020/home



Rust is a new programming language for writing performant code with strong type 
and memory safety guarantees. It is now considered a serious alternative to C 
and C++ for systems programming, because it provides high-level abstractions 
but without the cost of garbage collection. Given the growing popularity of 
Rust, and given that bugs in systems programs can be costly, there is growing 
interest in the program verification community for building program verifiers 
for Rust. In this workshop, we aim to bring together language designers, 
application developers and formal verification tool builders, to exchange ideas 
and build collaborations around developing verified Rust programs.

The goal of this workshop is to bring researchers from a variety of different 
backgrounds and perspectives together to exchange new and exciting ideas 
concerning the verification of Rust programs and exploring avenues for 
collaboration.

We want the workshop to be as informal and interactive as possible. The program 
will thus involve a combination of invited talks, contributed talks about work 
in progress, tool demos, and open-ended discussion sessions. There will be no 
published proceedings, but participants will be invited to submit working 
documents, talk slides, etc. to be posted on this website.



Call for Talk and Demo Proposals
-

We solicit proposals for contributed talks and tool demos. Proposals should be 
at most 2 pages, in either plain text or PDF format, and should specify how 
long a talk/demo the speaker wishes to give. By default, contributed talks will 
be 30 minutes long, but proposals for shorter or longer talks will also be 
considered.

We are interested in talks/demos on all topics related to the verification of 
Rust programs (including, for instance, program specification, deductive 
verification, model checking, symbolic execution, runtime monitoring, the 
semantics and formalization of Rust, and tool support). Talks about work in 
progress as well as proposals for challenge problems in Rust are particularly 
encouraged.

Please submit by email to 
peter.muel...@inf.ethz.ch.


Important Dates
-

Deadline for talk/demo proposals:  February 07, 2020 (Friday)
Notification of acceptance:  February 21, 2020 (Friday)
Workshop:   April 26, 2020 (Sunday)



Organizers


Rajeev Joshi, Amazon Web Services 
mailto:joraj...@amazon.com>>

Nicholas Matsakis, Mozilla mailto:nmatsa...@mozilla.com>>

Peter Müller, ETH Zurich 
mailto:peter.muel...@inf.ethz.ch>>

[TYPES/announce] Rust Verification Workshop at ETAPS 2020: Call for Talk, Demo, and Challenge Proposals

[Mueller Peter]

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

Call for Talk, Demo, and Challenge Proposals
1st Rust Verification Workshop

Co-located with ETAPS 2020
Dublin, Ireland
Sunday, 26 April, 2020
https://sites.google.com/view/rustverify2020/home



Rust is a new programming language for writing performant code with strong type 
and memory safety guarantees. It is now considered a serious alternative to C 
and C++ for systems programming, because it provides high-level abstractions 
but without the cost of garbage collection. Given the growing popularity of 
Rust, and given that bugs in systems programs can be costly, there is growing 
interest in the program verification community for building program verifiers 
for Rust. In this workshop, we aim to bring together language designers, 
application developers and formal verification tool builders, to exchange ideas 
and build collaborations around developing verified Rust programs.

The goal of this workshop is to bring researchers from a variety of different 
backgrounds and perspectives together to exchange new and exciting ideas 
concerning the verification of Rust programs and exploring avenues for 
collaboration.

We want the workshop to be as informal and interactive as possible. The program 
will thus involve a combination of invited talks, contributed talks about work 
in progress, tool demos, and open-ended discussion sessions. There will be no 
published proceedings, but participants will be invited to submit working 
documents, talk slides, etc. to be posted on this website.



Call for Talk and Demo Proposals
-

We solicit proposals for contributed talks and tool demos. Proposals should be 
at most 2 pages, in either plain text or PDF format, and should specify how 
long a talk/demo the speaker wishes to give. By default, contributed talks will 
be 30 minutes long, but proposals for shorter or longer talks will also be 
considered.

We are interested in talks/demos on all topics related to the verification of 
Rust programs (including, for instance, program specification, deductive 
verification, model checking, symbolic execution, runtime monitoring, the 
semantics and formalization of Rust, and tool support). Talks about work in 
progress as well as proposals for challenge problems in Rust are particularly 
encouraged.

Please submit by email to 
peter.muel...@inf.ethz.ch.


Important Dates
-

Deadline for talk/demo proposals:  February 07, 2020 (Friday)
Notification of acceptance:  February 21, 2020 (Friday)
Workshop:   April 26, 2020 (Sunday)



Organizers


Rajeev Joshi, Amazon Web Services 

Nicholas Matsakis, Mozilla 

Peter Müller, ETH Zurich 

[TYPES/announce] Assistant Professors at ETH Zurich: Security, Software Engineering, and Programming Languages

[Mueller Peter]

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

Assistant Professors (Tenure Track)
Security, Software Engineering, and Programming Languages
The Department of Computer Science (www.inf.ethz.ch) at ETH Zurich invites 
applications for assistant professorships (tenure track) in computer science 
with focus on different aspects of Cyber Security, Software Engineering, and 
Programming Languages.

- Privacy
- Programming Languages/Software Engineering
- Security of IT Infrastructure
- Software Security
- Trustworthy Software
- Education Technology (e.g. assignment generation, feedback and grading for 
programming and math assignments)

Please apply for only one of the above areas as all applications will be 
jointly reviewed.

Applicants should be strongly rooted in computer science, have internationally 
recognized expertise in their field and pursue research at the forefront of 
computer science. Successful candidates should establish and lead a strong 
research program. They will be expected to supervise doctoral students and 
teach both undergraduate and graduate level courses (in German or in English). 
Collaboration in research and teaching is expected both within the department 
and with other groups of ETH Zurich and related institutions.

Assistant professorships have been established to promote the careers of 
younger scientists. ETH Zurich implements a tenure track system equivalent to 
other top international universities.
See 
https://ethz.ch/en/the-eth-zurich/working-teaching-and-research/faculty-affairs/ausgeschriebene-professuren/ingenieurwissenschaften/assistant-professors--tenure-track--of-computer-science---securi.html
 for details.

[TYPES/announce] Multiple PhD and Postdoc positions in Information Security and Program Verification at ETH Zurich

[Mueller Peter]

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

The Institute of Information Security (the groups of Prof. Adrian Perrig and 
Prof. David Basin) and the Programming Methodology Group (Prof. Peter Müller) 
at ETH Zurich have multiple open positions for PhD students and Postdocs in a 
research project in the area of digital trust. The goal of this project is to 
develop a comprehensive, formally verified security architecture for 
communication in the physical and digital world. In particular, the project 
will develop protocols to transfer physical trust relationships into the 
digital world and store, manage, and use them. The design will take into 
account human (mis-)behavior from the outset. A particular emphasis is on the 
formal verification of the architecture both at the design and implementation 
level to rule out any undesired behavior.

We are looking for enthusiastic and outstanding Computer Science or Mathematics 
students and postdoctoral researchers with a strong background in some of the 
following topics:

 * formal modeling and verification,
 * program verification,
 * theorem proving, model checking,
 * cryptographic protocols,
 * public-key infrastructure, identity management, authentication,
 * networking and distributed systems, and
 * design and implementation of security architectures.

ETH Zurich regulations require PhD students to hold a Masters or equivalent 
degree (e.g., Diplom). All candidates matching the profile above are encouraged 
to apply as soon as possible. We will process applications until all positions 
are filled. Successful candidates are expected to start soon after acceptance, 
but the starting date is negotiable.

Applications should include:

- a curriculum vitae,
- a brief description of research interests,
- transcripts of grades,
- letters of recommendation from teachers or employers, and,
- if possible, the Master's or Bachelor's thesis and publications.

Applications and inquiries should be sent to Christoph Sprenger and Sandra 
Schneider at the following email addresses.

  infsec.positi...@inf.ethz.ch, jobs...@inf.ethz.ch 

PhD students and Postdocs are paid employees of ETH Zurich. Salary and 
employment conditions are attractive. Zurich is a diverse and multicultural 
city which is consistently rated among the best cities in the world in which to 
live.