[TYPES/announce] Call for Papers: HotSpot 2021

[Toby Murray]

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


HotSpot 2021:
7th Workshop on
Hot topics in the Principles of Security and Trust
Co-located with EuroS 2021, 7--11th September 2021 in Vienna, Austria
http://hotspot.compute.dtu.dk
Organized by the Theory of Security working group IFIP WG 1.7.


Aim and scope
=

The principles of security and trust remain an area of intense and
creative work.  This work is focused primarily on defining security
and trust goals, developing methods to verify that systems meet those
goals, and to synthesize systems that meet those goals by
construction.

The areas of interest for HotSpot cut across many application areas,
including hardware-software connections, vulnerability discovery
and program verification, distributed and cloud systems, big data,
machine learning for (and against) security and privacy, and
single-purpose systems such as voting, electronic currency and
smart contracts. The areas of interest are unified however by a
focus on rigorous models and reasoning, clear semantics,
and a balance between proof and empirical methods.

Format
==

The one-day workshop will be divided into a sequence of four main
sessions.  Some sessions will be devoted to a set of talks on related
topics, both with invited talks and submitted papers. We expect the
session topics to be drawn from the following list:

  Privacy and information flow
  Properties of voting protocols
  Machine-learning for (and against) security
  Hardware basis of security
  Vulnerability discovery and program verification
  Distributed ledger technologies
  Cyber-physical systems

Submissions on all formally-grounded topics related to security,
privacy and trust are welcome. They can either be

(a) an informal submission, consisting of an abstract or a paper that
may appear formally elsewhere.

(b) a full submission, to be included in an IEEE Xplore volume
accompanying the main IEEE EuroS 2021 proceedings.

See submission instructions on our website:
http://hotspot.compute.dtu.dk

PC
==

Catherine Meadows
Catuscia Palamidessi
Jan Juerjens
Jean-Jacques Quisquater
Joshua Guttman
Lucca Hirschi
Mark D. Ryan
Peter Y. A. Ryan
Pierpaolo Degano
Sebastian Mödersheim (co-chair)
Steve Schneider
Toby Murray (chair)


Important Dates
===

Workshop papers submission: May 02, 2021

Workshop notification date: June 01, 2021

Workshop final papers:  July 02, 2021

Workshop date: September 06, 2021

Submission instructions
===

See http://hotspot.compute.dtu.dk

[TYPES/announce] Postdoc position: verified timing-channel security for seL4

[Toby Murray]

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

Postdoc position: verified timing-channel security for seL4

http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

Applications close: February 25, 09:00 AM Australian Eastern Daylight
Time (AEDT; GMT +11)

Timing channels plague modern systems, undermining their security.
Yet no operating system provides provable protection against them.
We believe that seL4 can be the first kernel to meet this challenge [1],
building on its world-first proof of confidentiality enforcement [2]
and its unique mechanisms for implementing time protection [3].

The seL4 project is seeking a highly motivated postdoctoral
researcher to investigate methods for proving that operating system
kernels can defend against timing channels. We are seeking somebody
with a research background in formal methods and security.

You will contribute to the development of methods for reasoning about
timing channels in verified operating system kernels, applied to the
seL4 kernel. Your work will also investigate how to extend seL4’s
existing proofs of information flow security, which primarily cover
storage channels, to also encompass timing channels.

Further details about the research project are summarised in the
following position paper:

[1] Gernot Heiser, Gerwin Klein and Toby Murray.
"Can We Prove Time Protection?" in Proceedings of the
Workshop on Hot Topics in Operating Systems (HotOS),
pages 23-29, May 2019.
https://arxiv.org/abs/1901.08338

The position is for two years in the first instance, based at the
University of Melbourne under Dr Toby Murray
(https://people.eng.unimelb.edu.au/tobym/).  You will work with a
close-knit team here at University of Melbourne, and collaborate
heavily with UNSW and Data61’s Trustworthy Systems group, in Sydney.

Candidates should have experience in at least one of the following:
 - program verification (e.g. Hoare logic)
 - information flow security (e.g. non-interference)
 - interactive theorem provers (e.g. Isabelle, Coq, etc.)

Applications close on February 25, 09:00 AM Australian Eastern Daylight
Time (AEDT; GMT +11)

To apply, or fore more information, visit:

http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

Informal enquiries should be directed to
  Toby Murray
  toby.mur...@unimelb.edu.au
  https://people.eng.unimelb.edu.au/tobym/

References

[1] Gernot Heiser, Gerwin Klein and Toby Murray.
"Can We Prove Time Protection?", HotOS 2019

[2] Toby Murray, et al.
"seL4: From General Purpose to a Proof of Information
Flow Enforcement", IEEE Symposium on Security and Privacy 2013

[3] Qian Ge, Yuval Yarom, Tom Chothia, Gernot Heiser.
"Time Protection: The Missing OS Abstraction", EuroSys 2019

[TYPES/announce] Research Fellow in Verified Operating System Security

[Toby Murray]

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

Research Fellow in Verified Operating System Security
http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

The seL4 project and I am seeking a highly motivated postdoctoral
researcher to investigate methods for proving that operating system
kernels can defend against timing channels. We are seeking somebody
with a research background in formal methods and security.

You will contribute to the development of methods for reasoning about
timing channels in verified operating system kernels, applied to the
seL4 kernel. Your work will also investigate how to extend seL4’s
existing proofs of information flow security, which primarily cover
storage channels, to also encompass timing channels.

Further details about the research project are summarised in the
following position paper:

Gernot Heiser, Gerwin Klein and Toby Murray.
"Can We Prove Time Protection?" in Proceedings of the
Workshop on Hot Topics in Operating Systems (HotOS),
pages 23-29, May 2019.
https://arxiv.org/abs/1901.08338


The position is for two years in the first instance, based at the
University of Melbourne under Dr Toby Murray
(https://people.eng.unimelb.edu.au/tobym/).  You will work with a
close-knit team here at University of Melbourne, and collaborate
heavily with UNSW and Data61’s Trustworthy Systems group, in Sydney.

Candidates should have experience in at least one of the following:
 - program verification (e.g. Hoare logic)
 - information flow security (e.g. non-interference)
 - interactive theorem provers (e.g. Isabelle, Coq, etc.)

Applications close on August 30, 11:55pm Australian Eastern Standard
Time (GMT +10)
http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

Informal enquiries should be directed to
  Toby Murray
  toby.mur...@unimelb.edu.au
  https://people.eng.unimelb.edu.au/tobym/

[TYPES/announce] FTfJP 2019: CFP for Second Round

[Toby Murray]

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

# Call For Papers - Second Round

21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019)
https://conf.researchr.org/home/FTfJP-2019/

Monday 15th July 2019, London

Co-located with ECOOP 2019

## About FTfJP 2019

Formal techniques can help analyse programs, precisely describe
program behaviour, and verify program properties. Modern programming
languages are interesting targets for formal techniques due to their
ubiquity and wide user base, stable and well-defined interfaces and
platforms, and powerful (but also complex) libraries. New languages
and applications in this space are continually arising, resulting in
new programming languages (PL) research challenges.

Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each
other. FTfJP is an established workshop which has run annually since
1999 alongside ECOOP, with the goal of bringing together people
working in both fields.

The workshop has a broad PL theme; the most important criterion is
that submissions will generate interesting discussions within this
community. The term “Java-like” is somewhat historic and should be
interpreted broadly: FTfJP solicits and welcomes submission relating
to programming languages in general, beyond Java, C#, Scala, etc.

Example topics of interest include:

* Language design and semantics
* Type systems
* Concurrency and new application domains
* Specification and verification of program properties
* Program analysis (static or dynamic)
* Program Synthesis
* Security
* Pearls (programs or proofs)

FTfJP welcomes submissions on technical contributions, case studies,
experience reports, challenge proposals, and position papers.


## Submissions

Contributions are sought in two categories:

* Full Papers (6 pages, excluding references) present a technical
  contribution, case study, or detailed experience report. We welcome
  both complete and incomplete technical results; ongoing work is
  particularly welcome, provided it is substantial enough to stimulate
  interesting discussions.

* Short Papers (2 pages, excluding references) should advocate a
  promising research direction, or otherwise present a position likely
  to stimulate discussion at the workshop. We encourage
  e.g. established researchers to set out a personal vision, and
  beginning researchers to present a planned path to a PhD.

Both types of contributions will benefit from feedback received at the
workshop. Submissions will be peer reviewed, and will be evaluated
based on their clarity and their potential to generate interesting
discussions. The format of the workshop encourages interaction. FTfJP
is a forum in which a wide range of people share their expertise, from
experienced researchers to beginning PhD students.

Submissions are accepted via https://easychair.org/conferences/?conf=ftfjp2019


## Formatting and Publication

Submissions should be in acmart/sigplan style, 10pt font. Formatting
requirements are detailed on the SIGPLAN Author Information page
(https://www.sigplan.org/Resources/Author).

Accepted papers will be published in the ACM Digital Library by
default, though authors will be able to opt out of this publication,
if desired. At least one author of an accepted paper must attend the
workshop to present the work and participate in the discussions.

## Submission Rounds

Submissions will be taken in two rounds. Authors of papers
rejected in Round One are free to resubmit to Round Two in
either paper category, regardless of the type of Round One
submission.

## Important Dates

* Round One Submission Closes: 28 April (AoE)
* Roune One Notification: 20 May
* Round Two Submission Closes: 26 May (AoE)
* Round Two Notification: 10 June

## Invited Speakers

* Scott Owens (University of Kent): CakeML
* Philipp Ruemmer (Uppsala University): JayHorn

## Program Committee

* Yuyan Bao (Pennsylvania State University)
* James Bornholt (University of Washington)
* Gidon Ernst (Co-Chair; LMU Munich)
* Marie Farrell (University of Liverpool)
* Carlo A. Furia (USI – Università della Svizzera Italiana)
* Marie-Christine Jakobs (TU Darmstadt)
* Wojciech Mostowski (Halmstad University)
* Toby Murray (Co-Chair; University of Melbourne)
* Christine Rizkallah (University of New South Wales and Data61)
* Martin Schäf (Amazon Web Services)

[TYPES/announce] DEADLINE EXTENDED: FTfJP 2019 - 28 April

[Toby Murray]

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

# DEADLINE EXTENDED - CALL FOR PAPERS
Extended submission deadline: Sunday 28 April (AoE)

21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019)
https://conf.researchr.org/home/FTfJP-2019/

Monday 15th July 2019, London

Co-located with ECOOP 2019

## About FTfJP 2019

Formal techniques can help analyse programs, precisely describe
program behaviour, and verify program properties. Modern programming
languages are interesting targets for formal techniques due to their
ubiquity and wide user base, stable and well-defined interfaces and
platforms, and powerful (but also complex) libraries. New languages
and applications in this space are continually arising, resulting in
new programming languages (PL) research challenges.

Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each
other. FTfJP is an established workshop which has run annually since
1999 alongside ECOOP, with the goal of bringing together people
working in both fields.

The workshop has a broad PL theme; the most important criterion is
that submissions will generate interesting discussions within this
community. The term “Java-like” is somewhat historic and should be
interpreted broadly: FTfJP solicits and welcomes submission relating
to programming languages in general, beyond Java, C#, Scala, etc.

Example topics of interest include:

* Language design and semantics
* Type systems
* Concurrency and new application domains
* Specification and verification of program properties
* Program analysis (static or dynamic)
* Program Synthesis
* Security
* Pearls (programs or proofs)

FTfJP welcomes submissions on technical contributions, case studies,
experience reports, challenge proposals, and position papers.


## Submissions

Contributions are sought in two categories:

* Full Papers (6 pages, excluding references) present a technical
  contribution, case study, or detailed experience report. We welcome
  both complete and incomplete technical results; ongoing work is
  particularly welcome, provided it is substantial enough to stimulate
  interesting discussions.

* Short Papers (2 pages, excluding references) should advocate a
  promising research direction, or otherwise present a position likely
  to stimulate discussion at the workshop. We encourage
  e.g. established researchers to set out a personal vision, and
  beginning researchers to present a planned path to a PhD.

Both types of contributions will benefit from feedback received at the
workshop. Submissions will be peer reviewed, and will be evaluated
based on their clarity and their potential to generate interesting
discussions. The format of the workshop encourages interaction. FTfJP
is a forum in which a wide range of people share their expertise, from
experienced researchers to beginning PhD students.

Submissions are accepted via https://easychair.org/conferences/?conf=ftfjp2019


## Formatting and Publication

Submissions should be in acmart/sigplan style, 10pt font. Formatting
requirements are detailed on the SIGPLAN Author Information page
(https://www.sigplan.org/Resources/Author).

Accepted papers will be published in the ACM Digital Library by
default, though authors will be able to opt out of this publication,
if desired. At least one author of an accepted paper must attend the
workshop to present the work and participate in the discussions.


## Important Dates

* Submission: 28 April (AoE)
* Notification: 2 June

## Invited Speakers

* Scott Owens (University of Kent): CakeML
* Philipp Ruemmer (Uppsala University): JayHorn

## Program Committee

* Yuyan Bao (Pennsylvania State University)
* James Bornholt (University of Washington)
* Gidon Ernst (Co-Chair; LMU Munich)
* Marie Farrell (University of Liverpool)
* Carlo A. Furia (USI – Università della Svizzera Italiana)
* Marie-Christine Jakobs (TU Darmstadt)
* Wojciech Mostowski (Halmstad University)
* Toby Murray (Co-Chair; University of Melbourne)
* Christine Rizkallah (University of New South Wales and Data61)
* Martin Schäf (Amazon Web Services)

[TYPES/announce] FTfJP 2019: Second Call for Papers

[Toby Murray]

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

SECOND CALL FOR PAPERS
Submission deadline: Sunday 21 April (AoE)

21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019)
https://conf.researchr.org/home/FTfJP-2019/

Monday 15th July 2019, London

Co-located with ECOOP 2019

## About FTfJP 2019

Formal techniques can help analyse programs, precisely describe
program behaviour, and verify program properties. Modern programming
languages are interesting targets for formal techniques due to their
ubiquity and wide user base, stable and well-defined interfaces and
platforms, and powerful (but also complex) libraries. New languages
and applications in this space are continually arising, resulting in
new programming languages (PL) research challenges.

Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each
other. FTfJP is an established workshop which has run annually since
1999 alongside ECOOP, with the goal of bringing together people
working in both fields.

The workshop has a broad PL theme; the most important criterion is
that submissions will generate interesting discussions within this
community. The term “Java-like” is somewhat historic and should be
interpreted broadly: FTfJP solicits and welcomes submission relating
to programming languages in general, beyond Java, C#, Scala, etc.

Example topics of interest include:

* Language design and semantics
* Type systems
* Concurrency and new application domains
* Specification and verification of program properties
* Program analysis (static or dynamic)
* Program Synthesis
* Security
* Pearls (programs or proofs)

FTfJP welcomes submissions on technical contributions, case studies,
experience reports, challenge proposals, and position papers.


## Submissions

Contributions are sought in two categories:

* Full Papers (6 pages, excluding references) present a technical
  contribution, case study, or detailed experience report. We welcome
  both complete and incomplete technical results; ongoing work is
  particularly welcome, provided it is substantial enough to stimulate
  interesting discussions.

* Short Papers (2 pages, excluding references) should advocate a
  promising research direction, or otherwise present a position likely
  to stimulate discussion at the workshop. We encourage
  e.g. established researchers to set out a personal vision, and
  beginning researchers to present a planned path to a PhD.

Both types of contributions will benefit from feedback received at the
workshop. Submissions will be peer reviewed, and will be evaluated
based on their clarity and their potential to generate interesting
discussions. The format of the workshop encourages interaction. FTfJP
is a forum in which a wide range of people share their expertise, from
experienced researchers to beginning PhD students.

Submissions are accepted via https://easychair.org/conferences/?conf=ftfjp2019


## Formatting and Publication

Submissions should be in acmart/sigplan style, 10pt font. Formatting
requirements are detailed on the SIGPLAN Author Information page
(https://www.sigplan.org/Resources/Author).

Accepted papers will be published in the ACM Digital Library by
default, though authors will be able to opt out of this publication,
if desired. At least one author of an accepted paper must attend the
workshop to present the work and participate in the discussions.


## Important Dates

* Submission: 21 April (AoE)
* Notification: 2 June


## Program Committee

* Yuyan Bao (Pennsylvania State University)
* James Bornholt (University of Washington)
* Gidon Ernst (Co-Chair; LMU Munich)
* Marie Farrell (University of Liverpool)
* Carlo A. Furia (USI – Università della Svizzera Italiana)
* Marie-Christine Jakobs (TU Darmstadt)
* Wojciech Mostowski (Halmstad University)
* Toby Murray (Co-Chair; University of Melbourne)
* Christine Rizkallah (University of New South Wales and Data61)
* Martin Schäf (Amazon Web Services)

[TYPES/announce] Research Position in Verified Confidentiality for Weak Memory Concurrency

[Toby Murray]

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

Research Position in Verified Confidentiality for Weak Memory Concurrency
https://people.eng.unimelb.edu.au/tobym/researcher19-weak-memory.html

I am seeking an exceptional researcher (either a graduate or a
postdoc) to research methods for verifying information flow security
for shared-memory concurrent programs executing on weak memory
consistency models. The methods will be applied to verify the security
of seL4-based critical embedded devices.

The position is for two years in the first instance, based at the
University of Melbourne under Dr Toby Murray
(https://people.eng.unimelb.edu.au/tobym/). This project will provide
the opportunity to collaborate with researchers at Australian National
University (ANU), Canberra; Data61's Trustworthy Systems Group (the
"seL4 team"), Sydney; and Australia's Defence Science and Technology
(DST) Group, Brisbane.

Candidates should have experience in at least one of the following:
 - program verification (e.g. Hoare logic),
 - information flow security,
 - interactive proof assistants (e.g. Isabelle, Coq, etc.),
 - concurrent program verification methods (e.g. Owicki-Gries,
   Rely-Guarantee, Concurrent Separation Logic, etc.),
 - weak memory consistency models (e.g. x86 TSO, etc.)

The following are indicative, entry-level salary figures:
  Research Assistant (Bachelor's graduate): $65K (AUD)
  Research Assistant (Master's graduate): $71K (AUD)
  Postdoctoral Research Fellow: $90K (AUD)
Besides salary, total remuneration also includes 9.5% employer
superannuation contribution.

Applications close on April 30, 11:55pm Australian Eastern Standard
Time (GMT +10)

Further details, including how to apply, are available here:
https://people.eng.unimelb.edu.au/tobym/researcher19-weak-memory.html

Informal enquiries should be directed to
  Toby Murray
  toby.mur...@unimelb.edu.au
  https://people.eng.unimelb.edu.au/tobym/

[TYPES/announce] FTfJP 2019: Call for Papers

[Toby Murray]

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

# CALL FOR PAPERS

21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019)
https://conf.researchr.org/home/FTfJP-2019/

Co-located with ECOOP 2019, July 15-19, Hammersmith, London

## About FTfJP 2019

Formal techniques can help analyse programs, precisely describe
program behaviour, and verify program properties. Modern programming
languages are interesting targets for formal techniques due to their
ubiquity and wide user base, stable and well-defined interfaces and
platforms, and powerful (but also complex) libraries. New languages
and applications in this space are continually arising, resulting in
new programming languages (PL) research challenges.

Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each
other. FTfJP is an established workshop which has run annually since
1999 alongside ECOOP, with the goal of bringing together people
working in both fields.

The workshop has a broad PL theme; the most important criterion is
that submissions will generate interesting discussions within this
community. The term “Java-like” is somewhat historic and should be
interpreted broadly: FTfJP solicits and welcomes submission relating
to programming languages in general, beyond Java, C#, Scala, etc.

Example topics of interest include:

* Language design and semantics
* Type systems
* Concurrency and new application domains
* Specification and verification of program properties
* Program analysis (static or dynamic)
* Program Synthesis
* Security
* Pearls (programs or proofs)

FTfJP welcomes submissions on technical contributions, case studies,
experience reports, challenge proposals, and position papers.


## Submissions

Contributions are sought in two categories:

* Full Papers (6 pages, excluding references) present a technical
  contribution, case study, or detailed experience report. We welcome
  both complete and incomplete technical results; ongoing work is
  particularly welcome, provided it is substantial enough to stimulate
  interesting discussions.

* Short Papers (2 pages, excluding references) should advocate a
  promising research direction, or otherwise present a position likely
  to stimulate discussion at the workshop. We encourage
  e.g. established researchers to set out a personal vision, and
  beginning researchers to present a planned path to a PhD.

Both types of contributions will benefit from feedback received at the
workshop. Submissions will be peer reviewed, and will be evaluated
based on their clarity and their potential to generate interesting
discussions. The format of the workshop encourages interaction. FTfJP
is a forum in which a wide range of people share their expertise, from
experienced researchers to beginning PhD students.


## Formatting and Publication

Submissions should be in acmart/sigplan style, 10pt font. Formatting
requirements are detailed on the SIGPLAN Author Information page
(https://www.sigplan.org/Resources/Author).

Accepted papers will be published in the ACM Digital Library by
default, though authors will be able to opt out of this publication,
if desired. At least one author of an accepted paper must attend the
workshop to present the work and participate in the discussions.


## Important Dates

* Submission: 21 April (AoE)
* Notification: 2 June


## Program Committee

* Yuyan Bao (Pennsylvania State University)
* James Bornholt (University of Washington)
* Gidon Ernst (Co-Chair; LMU Munich)
* Marie Farrell (University of Liverpool)
* Carlo A. Furia (USI – Università della Svizzera Italiana)
* Marie-Christine Jakobs (TU Darmstadt)
* Wojciech Mostowski (Halmstad University)
* Toby Murray (Co-Chair; University of Melbourne)
* Christine Rizkallah (University of New South Wales and Data61)
* Martin Schäf (Amazon Web Services)

[TYPES/announce] Research position in Verified Confidentiality for Weak Memory Concurrency, Melbourne

[Toby Murray]

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

[apologies if you receive multiple copies of this message]

I am seeking an exceptional researcher (Research Assistant or
postdoctoral Research Fellow) to research methods for verifying
information flow security for shared-memory concurrent programs
executing on weak memory consistency models.

The position is for one year in the first instance, to begin in the
first quarter of 2019, based at the University of Melbourne under
Dr Toby Murray (https://people.eng.unimelb.edu.au/tobym/). This project
will provide the opportunity to collaborate with researchers at
Australian National University (ANU), Canberra; Data61's Trustworthy
Systems Group (the "seL4 team"), Sydney; and Australia's Defence
Science and Technology (DST) Group, Brisbane.

Research Assistants (respectively postdoctoral Research Fellows) would
have a degree (respectively PhD) in Computer Science or a closely
related field.

Candidates should have experience in at least one of the following:
 - program verification / formal methods,
 - information flow security,
 - concurrency,
 - the Isabelle theorem prover.

The following are indicative, entry-level salary figures:
  Research Assistant: $65,029 (AUD)
  Postdoctoral Research Fellow: $90,037 (AUD)
Besides salary, total remuneration also includes 9.5% employer
superannuation contribution.

Interested candidates should contact Toby Murray
(toby.mur...@unimelb.edu.au) in the first instance.

[TYPES/announce] Lecturer/Senior Lecturer (Continuing) at Univerity of Melbourne

[Toby Murray]

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

The University of Melbourne is currently advertising a continuing
(tenure track) Lecturer / Senior Lecturer position in Cybersecurity,
one of whose primary focus areas includes formal methods for
verification. You can find the job ad here and reproduced below:
http://jobs.unimelb.edu.au/caw/en/job/897514/academic-opportunities-cyber-security

Feel free to direct informal enquiries about the school to Toby Murray
(toby.mur...@unimelb.edu.au)

-

ACADEMIC OPPORTUNITIES - CYBER SECURITY

Job no: 0046468
Work type: Continuing
Location: Parkville
Division/Faculty: Melbourne School of Engineering
Department/School: School of Computing and Information Systems
Salary: $120,993 - $139,510 (Level C)
Role & Superannuation rate: Academic - 17% superannuation

School of Computing and Information Systems
Melbourne School of Engineering

Salary: $98,775 - $117,290 p.a. (Level B) OR $120,993 - $139,510 p.a.
(Level C) plus 17% superannuation

About Melbourne School of Engineering (MSE)
At MSE, we are committed to excellence. We are transforming our
engineering and IT teaching and research at the University of
Melbourne, guided by MSE 2025, our ten-year strategic plan. With an
expected investment of $1 billion in people and infrastructure, we are
creating the entrepreneurial leaders and technology of the future —
the people and things that will drive innovation and productivity to
make a sustainable impact on the world in which we live. It’s an
incredibly exciting time to be joining MSE!

About the School of Computing and Information Systems (CIS)
We are international research leaders with a focus on delivering
impact and making a real difference in three key areas: data and
knowledge, platforms and systems, and people and organisations. In
this discipline, the School was ranked number 1 in Australia and 14th
in the world in the 2018 QS World University Ranking exercise. At the
School of Computing and Information Systems, you'll find smart people,
big problems, and plenty of opportunities to make a real difference in
the world.

The Opportunity
We are now inviting outstanding academic talent from around the world
with expertise in cyber security ranging from cyber security topics
including; artificial intelligence, machine learning, cryptography and
privacy, security management, distributed systems and network security
to join our growing school.

With permanent positions available for both Lecturers and Senior
Lecturers, our academics have the opportunity to help to enrich our
collaborative, interdisciplinary research and teaching across our
departments. We encourage you to share your passion with the next
generation of leaders. We look for an ability to engage in thoughts of
new and exciting ways to help the growth and development of our
students, so that with your guidance we can empower them to unlock
their full potential.

Whilst these areas are of particular interest, exceptional candidates
from all areas of computer science and information systems will be
considered especially those with research experience in:

Security analytics
Cryptography and privacy
Security management
Distributed systems and network security
Formal methods for verification

Excitingly, you will also make a significant contribution to the
University of Melbourne Academic Centre for Cybersecurity Excellence
(UoM ACCSE) an initiative of the Commonwealth Government through the
Department of Education and Training and one of only two such centres
in Australia.

What you’ll be doing
You will be encouraged to collaborate in research within the School,
the University, and industry and government agencies. You will be an
aspiring leader in Computer Science or Information Systems research,
with ambition to publish in top quality journals and conferences,
mentor research students, and secure independent grant funding to
support a program of research. You will be expected to develop a
research portfolio and contribute to teaching in graduate and
undergraduate programs within the School.

What we offer you
Apart from competitive salaries, our benefits are aimed at recognising
and rewarding the contributions you make. We offer complete
flexibility, whatever that may mean for you. Many of our benefit
programs and onsite amenities are aimed at supporting you - including
generous leave, child care subsidies, discounted parking, medical and
health care. We offer extensive opportunities for personal and
professional development and we’ll support you in doing what you love.

Academics who regularly engage in practice-developing research and
development activities and have a strong track record of working well
in academic teams and independently are encouraged to apply

How to Apply

Apply online and complete the detailed application form.
You are not required to upload a resume or address the selection
criteria for this position.
You are only requ

[TYPES/announce] 15 Faculty Positions at University of Melbourne

[Toby Murray]

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

The University of Melbourne School of Computing and Information
Systems is seeking applicants for 15 continuing (tenure-track)
Lecturer and Senior Lecturer positions. We seek dynamic academics with
expertise in Computer Science or Information Systems who have the
potential to build a stellar teaching and research career at
Melbourne.

The School of Computing and Information Systems is an international
research leader in computer science, information systems and software
engineering. In this discipline, the School was ranked number 1 in
Australia and 13th in the world in the 2016 QS World University
Ranking exercise.

We are particularly seeking applicants with expertise in the areas of
business information systems, health informatics/digital health,
software engineering, cybersecurity, or high-performance and
distributed systems, but applicants whose work is aligned with any of
the research groups in the School are encouraged to apply.

Applications close on 15 Jan 2018. The positions are advertised at
http://go.unimelb.edu.au/jsp6, where the formal position description
and a brochure with more information are available.

Contact Karin Verspoor  for enquiries
and further information.

[TYPES/announce] Research (postdoc or graduate) position in Program Verification and Security

[Toby Murray]

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

Dear all

[Please spread the word to folks you believe may be interested.
 Apologies if you receive multiple copies of this message.]

I'm currently recruiting a researcher (a postdoc or a graduate with
suitable experience), to work on the application of concurrent
separation logic for verifying information flow security of
seL4-based, security-critical embedded systems. Verified information
flow security has seen something of a renaissance over the past 5
years, with success stories such as seL4 or the more recent mCertiKOS;
but concurrency remains an open challenge and one that this project
aims to address for the first time.

This research will:

  1. design and mechanise logics for verifying the information flow
 security of concurrent programs, and
  2. apply those logics to verify software running on seL4-based,
 user-facing critical embedded devices, previously deployed on
 Defence networks to process and protect classified information.

Ideal applicants will have prior experience with an interactive
theorem prover like Isabelle or Coq, and either knowledge of
verification techniques for shared memory concurrent programs
(e.g. rely guarantee, concurrent separation logic, etc.) or
information flow security (noninterference, declassification, etc.).

The successful applicant will be based at the University of Melbourne
and work in collaboration with project partners at Data61's
Trustworthy Systems group in Sydney (http://ts.data61.csiro.au/) and
the Defence Science and Technology Group in Adelaide.

The position is currently funded for one year, beginning around
July--September 2017, with possible extension beyond 12 months
contingent on additional funding.

Applications close on the 28th of May, Australian Eastern Standard
Time (AEST, GMT +10 hours), and should be made on-line:
  
http://jobs.unimelb.edu.au/caw/en/job/890645/research-assistant-research-fellow-in-program-verification-security

Applicants are encouraged to contact me in the first instance.

Enquiries about the position should be directed to:
  Toby Murray
  toby.mur...@unimelb.edu.au
  http://people.eng.unimelb.edu.au/tobym/

Thanks heaps

Toby

[TYPES/announce] SSV 2015 - Deadline Extended to Oct 5th

[Toby Murray]

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


SSV 2015 Final Call for Papers -- Deadline Extended

http://www.ssv-conference.org/

9th Conference on Systems Software Verification

Gold Coast, Australia, December 7-8, 2015
co-located with ICECCS.



Important Dates

Paper Submission: October 5, 2015 at
https://www.easychair.org/conferences/?conf=ssv2015
Notification: October 30, 2015
Conference: December 7–8, 2015


Topics

Industrial-strength software analysis and verification has advanced in
recent years through the introduction of model checking, automated and
interactive theorem proving, and static analysis techniques, as well as
correctness by design, correctness by contract, and model-driven
development. However, many techniques are working under restrictive
assumptions that are invalidated by complex embedded systems software
such as operating system kernels, low-level device drivers, or
microcontroller code.

The aim of this conference is to bring together researchers and
developers from both academia and industry who are facing real software
and real problems with the goal of finding real, applicable solutions.
By “real” we mean problems such as time-to-market or reliability that
the industry is facing. A real solution is one that is applicable to the
problem in industry and not one that only applies to an abstract,
academic, toy version of it. In this event we will discuss software
analysis and development techniques and tools; this forum will serve as
a platform to discuss open problems and future challenges in dealing
with existing and upcoming systems-level code.

Topics include, but are not restricted to:

* Model checking
* Automated and interactive theorem proving
* Static analysis and type systems
* Automated testing
* Model-driven development
* Concurrency
* Security
* Embedded systems development
* Programming languages
* Verifying compilers
* Software certification
* Software tools
* Experience reports


Submissions

Submissions must be made electronically through the EasyChair system
until October 5th, 2015. Papers should be up to 10 pages in pdf
format and formatted in EPTCS style [http://info.eptcs.org]. Additional
details may be included in a clearly marked appendix, which will be read
at the discretion of the program committee. All will be subject to peer
review under normal conference standards. Experience reports and papers
on work in progress are welcome as long as there is a clear
contribution. Submissions which are based or discuss a non-trivial piece
of software are required to make all those non-standard software parts
available, which a referee may need, in order to check the claims of the
submission.

Submitted papers must not have previously appeared in a journal or
conference with published proceedings and must not be concurrently
submitted to any other peer-reviewed workshop, symposium, conference or
archival journal. Any partial overlap with any such published or
concurrently submitted paper must be clearly indicated.


Proceedings

Proceedings will be published as an issue in Electronic Proceedings in
Theoretical Computer Science.


Program Committee

Jade Alglave, University College London
Ezio Bartocci, TU Wien
Andrew Butterfield, Lero, Trinity College Dublin
Franck Cassez, Macquarie University
Ana Cavalcanti, University of York
Mads Dam, KTH Royal Institute of Technology
Alastair Donaldson, Imperial College London
Stefania Gnesi, ISTI
Chris Hawblitzel, Microsoft Research
Jérome Hugues, ISAE
Limin Jia, CMU
Tiziana Margaria, Lero, University of Limerick
Toby Murray, NICTA and UNSW (Co-Chair)
John Regehr, University of Utah
David Sanán, NTU (Co-Chair)
Konrad Slind, Rockwell Collins
Jun Sun, SUTD
Alwen Tiu, NTU
Mark van den Brand, Eindhoven University of Technology


Steering Committee

Ralf Huuck, NICTA and UNSW
Gerwin Klein, NICTA and UNSW
Bastian Schlich, ABB Corporate Research

[TYPES/announce] SSV 2015 - 2nd Call for Papers

[Toby Murray]

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


SSV 2015 2nd Call for Papers

http://www.ssv-conference.org/

9th Conference on Systems Software Verification

Gold Coast, Australia, December 7-8, 2015
co-located with ICECCS.



Important Dates

Abstract Submission: September 21, 2015 at
https://www.easychair.org/conferences/?conf=ssv2015
Paper Submission: September 28, 2015 at
https://www.easychair.org/conferences/?conf=ssv2015
Notification: October 30, 2015
Conference: December 7–8, 2015


Topics

Industrial-strength software analysis and verification has advanced in
recent years through the introduction of model checking, automated and
interactive theorem proving, and static analysis techniques, as well as
correctness by design, correctness by contract, and model-driven
development. However, many techniques are working under restrictive
assumptions that are invalidated by complex embedded systems software
such as operating system kernels, low-level device drivers, or
microcontroller code.

The aim of this conference is to bring together researchers and
developers from both academia and industry who are facing real software
and real problems with the goal of finding real, applicable solutions.
By “real” we mean problems such as time-to-market or reliability that
the industry is facing. A real solution is one that is applicable to the
problem in industry and not one that only applies to an abstract,
academic, toy version of it. In this event we will discuss software
analysis and development techniques and tools; this forum will serve as
a platform to discuss open problems and future challenges in dealing
with existing and upcoming systems-level code.

Topics include, but are not restricted to:

* Model checking
* Automated and interactive theorem proving
* Static analysis and type systems
* Automated testing
* Model-driven development
* Concurrency
* Security
* Embedded systems development
* Programming languages
* Verifying compilers
* Software certification
* Software tools
* Experience reports


Submissions

Submissions must be made electronically through the EasyChair system
until September 28th, 2015. Papers should be up to 10 pages in pdf
format and formatted in EPTCS style [http://info.eptcs.org]. Additional
details may be included in a clearly marked appendix, which will be read
at the discretion of the program committee. All will be subject to peer
review under normal conference standards. Experience reports and papers
on work in progress are welcome as long as there is a clear
contribution. Submissions which are based or discuss a non-trivial piece
of software are required to make all those non-standard software parts
available, which a referee may need, in order to check the claims of the
submission.

Submitted papers must not have previously appeared in a journal or
conference with published proceedings and must not be concurrently
submitted to any other peer-reviewed workshop, symposium, conference or
archival journal. Any partial overlap with any such published or
concurrently submitted paper must be clearly indicated.


Proceedings

Proceedings will be published as an issue in Electronic Proceedings in
Theoretical Computer Science.


Program Committee

Jade Alglave, University College London
Ezio Bartocci, TU Wien
Andrew Butterfield, Lero, Trinity College Dublin
Franck Cassez, Macquarie University
Ana Cavalcanti, University of York
Mads Dam, KTH Royal Institute of Technology
Alastair Donaldson, Imperial College London
Stefania Gnesi, ISTI
Chris Hawblitzel, Microsoft Research
Jérome Hugues, ISAE
Limin Jia, CMU
Tiziana Margaria, Lero, University of Limerick
Toby Murray, NICTA and UNSW (Co-Chair)
John Regehr, University of Utah
David Sanán, NTU (Co-Chair)
Konrad Slind, Rockwell Collins
Jun Sun, SUTD
Alwen Tiu, NTU
Mark van den Brand, Eindhoven University of Technology


Steering Committee

Ralf Huuck, NICTA and UNSW
Gerwin Klein, NICTA and UNSW
Bastian Schlich, ABB Corporate Research



The information in this e-mail may be confidential and subject to
legal professional privilege and/or copyright. National ICT Australia
Limited accepts no liability for any damage caused by this email or
its attachments.

[TYPES/announce] SSV 2015 - Call for Papers

[Toby Murray]

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


SSV 2015 Call for Papers

http://www.ssv-conference.org/

9th Conference on Systems Software Verification

Gold Coast, Australia, December 7-8, 2015
co-located with ICECCS.



Important Dates

Abstract Submission: September 21, 2015 at
https://www.easychair.org/conferences/?conf=ssv2015
Paper Submission: September 28, 2015 at
https://www.easychair.org/conferences/?conf=ssv2015
Notification: October 30, 2015
Conference: December 7–8, 2015


Topics

Industrial-strength software analysis and verification has advanced in
recent years through the introduction of model checking, automated and
interactive theorem proving, and static analysis techniques, as well
as correctness by design, correctness by contract, and model-driven
development. However, many techniques are working under restrictive
assumptions that are invalidated by complex embedded systems software
such as operating system kernels, low-level device drivers, or
microcontroller code.

The aim of this conference is to bring together researchers and
developers from both academia and industry who are facing real
software and real problems with the goal of finding real, applicable
solutions. By “real” we mean problems such as time-to-market or
reliability that the industry is facing. A real solution is one that
is applicable to the problem in industry and not one that only applies
to an abstract, academic, toy version of it. In this event we will
discuss software analysis and development techniques and tools; this
forum will serve as a platform to discuss open problems and future
challenges in dealing with existing and upcoming systems-level code.

Topics include, but are not restricted to:

* Model checking
* Automated and interactive theorem proving
* Static analysis and type systems
* Automated testing
* Model-driven development
* Concurrency
* Security
* Embedded systems development
* Programming languages
* Verifying compilers
* Software certification
* Software tools
* Experience reports


Submissions

Submissions must be made electronically through the EasyChair system
until September 28th, 2015. Papers should be up to 10 pages in pdf
format and formatted in EPTCS style [http://info.eptcs.org].
Additional details may be included in a clearly marked appendix, which
will be read at the discretion of the program committee. All will be
subject to peer review under normal conference standards. Experience
reports and papers on work in progress are welcome as long as there is
a clear contribution. Submissions which are based or discuss a
non-trivial piece of software are required to make all those
non-standard software parts available, which a referee may need, in
order to check the claims of the submission.

Submitted papers must not have previously appeared in a journal or
conference with published proceedings and must not be concurrently
submitted to any other peer-reviewed workshop, symposium, conference
or archival journal. Any partial overlap with any such published or
concurrently submitted paper must be clearly indicated.


Proceedings

Proceedings will be published as an issue in Electronic Proceedings in
Theoretical Computer Science.


Program Committee

Jade Alglave, University College London
Ezio Bartocci, TU Wien
Andrew Butterfield, Lero, Trinity College Dublin
Franck Cassez, Macquarie University
Ana Cavalcanti, University of York
Mads Dam, KTH Royal Institute of Technology
Alastair Donaldson, Imperial College London
Stefania Gnesi, ISTI
Chris Hawblitzel, Microsoft Research
Jérome Hugues, ISAE
Limin Jia, CMU
Tiziana Margaria, Lero, University of Limerick
Toby Murray, NICTA and UNSW (Co-Chair)
John Regehr, University of Utah
David Sanán, NTU (Co-Chair)
Konrad Slind, Rockwell Collins
Jun Sun, SUTD
Alwen Tiu, NTU
Mark van den Brand, Eindhoven University of Technology


Steering Committee

Ralf Huuck, NICTA and UNSW
Gerwin Klein, NICTA and UNSW
Bastian Schlich, ABB Corporate Research

[TYPES/announce] Call for Papers: SSV 2014

[Toby Murray]

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


SSV 2014 Call for Papers
 http://www.ssv-conference.org/

 8th International Workshop on
 Systems Software Verification

Vienna, July 23-24, 2014
  co-located with CAV and ITP,
  as part of the Vienna Summer of Logic 2014.


Important Dates
===
Paper Submission: April 1, 2014
Notification: May 1, 2014
Conference: July 23-24, 2014

Topics
==
Industrial-strength software analysis and verification has advanced in
recent years through the introduction of model checking, automated and
interactive theorem proving, and static analysis techniques, as well as
correctness by design, correctness by contract, and model-driven
development. However, many techniques are working under restrictive
assumptions that are invalidated by complex embedded systems software
such as operating system kernels, low-level device drivers, or
microcontroller code.

The aim of this workshop is to bring together researchers and developers
from both academia and industry who are facing real software and real
problems with the goal of finding real, applicable solutions. By real
we mean problems such as time-to-market or reliability that the industry
is facing. A real solution is one that is applicable to the problem in
industry and not one that only applies to an abstract, academic, toy
version of it. In this workshop we will discuss software analysis and
development techniques and tools; this forum will serve as a platform to
discuss open problems and future challenges in dealing with existing and
upcoming systems-level code.

Topics include, but are not restricted to:
* Model checking
* Automated and interactive theorem proving
* Static analysis
* Automated testing
* Model-driven development
* Embedded systems development
* Programming languages
* Verifying compilers
* Software certification
* Software tools
* Experience reports

Submissions
===
Submissions must be made electronically through the EasyChair system
[https://www.easychair.org/conferences/?conf=ssv2014] until April 1st,
2014. Papers should be up to 10 pages in pdf format and formatted in
EPTCS style [http://info.eptcs.org/]. Additional details may be included
in a clearly marked appendix, which will be read at the discretion of
the program committee. All will be subject to peer review under normal
conference standards. Experience reports and papers on work in progress
are welcome as long as there is a clear contribution. Submissions which
are based or discuss a non-trivial piece of software are required to
make all those non-standard software parts available, which a referee
may need, in order to check the claims of the submission.

Submitted papers must not have previously appeared in a journal or
conference with published proceedings and must not be concurrently
submitted to any other peer-reviewed workshop, symposium, conference or
archival journal. Any partial overlap with any such published or
concurrently submitted paper must be clearly indicated.

PC Chairs
=
Kim G. Larsen, AAU, Aalborg, Denmark
Mads Chr. Olesen, AAU, Aalborg, Denmark

Program Committee
=
Alessandro Coglio, Kestrel Institute
Björn Lisper, Mälardalen University
Cyrille Valentin Artho, AIST
Frédéric Boniol, ONERA
Heiko Falk, Ulm University
Jan Peleska, TZI, Universitat Bremen, Germany
Joe Leslie-Hurd, Intel Corporation
John Regehr, University of Utah
Jun Sun, Singapore University of Technology and Design
Martin Schoeberl, Technical University of Denmark
Natarajan Shankar, SRI International
Raimund Kirner, University of Hertfordshire
Stefan Berghofer, secunet Security Networks AG
Thomas Kropf, University of Tübingen
Toby Murray, NICTA

Steering Committee
==
R. Huuck, NICTA and UNSW, Sydney, Australia
G. Klein, NICTA and UNSW, Sydney, Australia
B. Schlich, ABB Corporate Research, Ladenburg, Germany