[TYPES/announce] PhD position on Embedded Systems Verification at University of Twente, Netherlands

[m.huis...@utwente.nl]

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

We are looking for a PhD candidate for a 4-year project on Formal Methods for 
Embedded Systems, as part of SAVES (ScAlable Verification of industrial 
Embedded control Systems), a collaboration with the University of Münster (WWU 
Münster). You will be working on the SAVES project, carried out in 
collaboration with prof. dr. Paula Herber (University of Twente / WWU Münster).

The overall goal of SAVES is to investigate methods and tools to establish 
correctness of embedded systems. With trends such as Industry 4.0, the internet 
of things, and autonomous driving, the complexity of embedded systems is 
steadily increasing. A prerequisite to ensure the correct functioning of 
industrial embedded systems under all circumstances is a clear understanding of 
the models and languages that are used in the development process. Formal 
methods provide a basis to make the development process systematic, 
well-defined, and automated. However, for many industrially relevant languages 
and models, the semantics are only informally defined. Together with the 
limited scalability of formal design and verification techniques, this makes 
the formal verification of industrial embedded control systems a difficult 
challenge, which can not be solved satisfactory with currently available 
methods and tools. At the same time, we see that in the area of deductive 
program verification, powerful techniques and tools have been developed to 
reason about software with unbounded parameters, for example the VerCors tool 
suite. In this project, we will extend these techniques with concepts to cope 
with heterogeneity, concurrency, and real-time to make them suitable for 
industrial embedded systems.

The PhD candidate hired at the University of Twente will be supervised by 
Marieke Huisman and Paula Herber and will work on extensions of the methods and 
tools developed in the FMT group for embedded systems, in close collaboration 
with the Embedded Systems group in Münster.

For further information about the group, see 
https://www.utwente.nl/en/eemcs/fmt/. For further information about the 
project, see https://www.utwente.nl/en/eemcs/fmt/research/projects/saves/.

YOUR PROFILE


  *   You have a MSc degree in Computer Science (or equivalent);
  *   You have a thorough theoretical background and a demonstrable interest in 
embedded or cyber-physical systems, and ideally some prior experience with 
embedded systems design, formal methods, and/or interactive theorem provers;
  *   You are an enthusiastic student, skilled in exact and abstract thinking;
  *   You are proficient in English on an academic level.

OUR OFFER

The terms of employment are in accordance with the Dutch Collective Labour 
Agreement for Universities (CAO) and include:


  *   A fulltime PhD position for four years, with a qualifier in the first 
year;
  *   Full status as an employee at the UT, including pension and health care 
benefits;
  *   The salary will range from € 2.395 (1st year) to € 3.061,- (4th year) per 
month, plus a holiday allowance of 8% and a year-end bonus of 8.3%;
  *   A solid pension scheme;
  *   Excellent facilities for professional and personal development;
  *   A green and lively campus, with lots of sports facilities and other 
activities.

INFORMATION AND APPLICATION

Are you interested in this position? Please send your application via 
https://www.utwente.nl/en/organisation/careers/!/2021-425/phd-position-on-embedded-systems-
 before 5th of July and include:


  *   A cover letter (explaining your specific interest and qualifications);
  *   A detailed Curriculum Vitae;
  *   A list of all courses + marks and a short description of your MSc thesis;
  *   References (contact information) of two scientific staff members.


The deadline of application is July 5, 2021 or until the position is filled. 
Starting date of the position is as soon as possible, or to be discussed.

For further information, you can contact Prof.dr.ir. Paula Herber: 
https://www.uni-muenster.de/EmbSys/team/herber/ or Prof.dr. Marieke Huisman: 
https://wwwhome.ewi.utwente.nl/~marieke/

DEPARTMENT
In the Formal Methods and Tools (FMT) research group, formal techniques and 
tools are developed and used as a means to support the development of software. 
Our central goal is to increase the reliability of the software that we rely 
on, as individuals and as society. We primarily target complex concurrent ICT 
systems, embedded in a technological context or in a distributed environment.

The FMT group is part of the Faculty of Electrical Engineering, Mathematics and 
Computer Science (EEMCS) at the University of Twente. The FMT group also 
participates in the Digital Systems Institute (DSI).

Our institute was ranked first at the most recent research national assessment.

ORGANIZATION
The faculty of Electrical Engineering, Mathematics and Computer Science 

[TYPES/announce] IFL2021 second call for papers

[Pieter Koopman]

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



IFL 2021

33rd Symposium on Implementation and Application of Functional Languages


 venue: online
  1 - 3 September 2021

 https://ifl21.cs.ru.nl




News


   - Paper submission is now open:
   https://easychair.org/conferences/?conf=ifl21
   

   .
   - Invited speakers are added: Stephanie Weirich and John Hughes
   - Sponsor added:  Facebook Research
   




Scope

The goal of the IFL symposia is to bring together researchers actively
engaged
in the implementation and application of functional and function-based
programming languages. IFL 2021 will be a venue for researchers to present
and
discuss new ideas and concepts, work in progress, and publication-ripe
results
related to the implementation and application of functional languages and
function-based programming.


Industrial track and topics of interest

This year's edition of IFL explicitly solicits original work concerning
*applications*
of functional programming in industry and academia. These contributions
will be reviewed by experts with an industrial background.

Topics of interest to IFL include, but are not limited to:

* language concepts
* type systems, type checking, type inferencing
* compilation techniques
* staged compilation
* run-time function specialisation
* run-time code generation
* partial evaluation
* (abstract) interpretation
* meta-programming
* generic programming
* automatic program generation
* array processing
* concurrent/parallel programming
* concurrent/parallel program execution
* embedded systems
* web applications
* (embedded) domain-specific languages
* security
* novel memory management techniques
* run-time profiling performance measurements
* debugging and tracing
* testing and proofing
* virtual/abstract machine architectures
* validation, verification of functional programs
* tools and programming techniques
* applications of functional programming in the industry, including
** functional programming techniques for large applications
** successes of the application functional programming
** challenges for functional programming encountered
** any topic related to the application of functional programming that is
interesting for the IFL community


Post-symposium peer-review

Following IFL tradition, IFL 2021 will use a post-symposium review process
to
produce the formal proceedings.

Before the symposium authors submit draft papers. These draft papers will
be
screened by the program chairs to make sure that they are within the scope
of
IFL. The draft papers will be made available to all participants at the
symposium.
Each draft paper is presented by one of the authors at the symposium.

After the symposium every presenter is invited to submit a full paper,
incorporating feedback from discussions at the symposium. Work submitted to
IFL
may not be simultaneously submitted to other venues; submissions must
adhere to ACM SIGPLAN's republication policy. The program committee will
evaluate these submissions according to their correctness, novelty,
originality,
relevance, significance, and clarity, and will thereby determine whether
the
paper is accepted or rejected for the formal proceedings. We plan to
publish
these proceedings in the International Conference Proceedings Series of the
ACM Digital Library, as in previous years. Moreover, the proceedings will
also
be made publicly available as open access.


Important dates

Submission deadline of draft papers:   17 August 2021
Notification of acceptance for presentation:   19 August 2021
Registration deadline: 30 August 2021
IFL Symposium: 1-3 September 2021
Submission of papers for proceedings:  6 December 2021
Notification of acceptance:3 February 2022
Camera-ready version:  15 March 2022


Submission details

All contributions must be written in English. Papers must use the ACM two
columns conference format, which can be found at:

  http://www.acm.org/publications/proceedings-template

[TYPES/announce] CAV 2021 Student Fellowships

[Thomas Wies]

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

---
Call for Applications

CAV 2021 Student Fellowships
---

Important Dates
---

Application deadline: July 2, 2021
Notification: July 7, 2021
Conference: July 18-14, 2021

Application Form


https://forms.gle/wrpY9eKyNEA8gog39

Objectives
--

CAV 2021 is the 33rd in a series dedicated to the advancement of the 
theory and practice of computer-aided formal analysis methods for 
hardware and software systems. The conference will take place virtually 
18-24, 2021.


CAV has some funds from the National Science Foundation to cover the 
registration fee for student attendees of CAV'21 that are studying at a 
US university.


The application deadline is July 2, 2021, and recipients will be 
notified by July 7.


Funds will be provided after the conference, upon submission of the 
receipt for the CAV registration and a short report detailing the 
student's experience at and benefit from CAV'21 (these reports will be 
used to compile a final report to our sponsors).


Special efforts will be made to bring to CAV students from 
under-represented groups. Applications from first-year PhD students and 
undergraduate students interested in formal methods are particularly 
encouraged.


Applications must be received by the deadline. Applicants are required 
to apply using the following web form:


https://forms.gle/wrpY9eKyNEA8gog39

If you have questions, please contact cav2021fellows...@gmail.com.

Thomas Wies
(CAV'21 Fellowship Chair)

[TYPES/announce] Postdoc Position in Formal Security Analysis of Cryptographic Protocols and Web Applications, University of Stuttgart, Germany

[Ralf Kuesters]

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

The Institute of Information Security at University of Stuttgart offers a

fully-funded Postdoc position.

The successful candidate is expected to work on tool-supported formal
analysis of cryptographic protocols and web applications building, among
others, on our work published at EuroS 2021, S 2019, CSF 2017, CCS
2016, CCS 2015, ESORICS 2015, and S 2014. One goal is to provide
tool-supported security analysis based on DY* for our web infrastructure
model (WIM).

The position is available immediately with an internationally
competitive salary (German public salary scale TV-L E13 or TV-L E14,
depending on the candidate's qualification).  The appointment period
follows the German Wissenschaftszeitvertragsgesetz (WissZeitVg), ranging
from one year to up to six years.

The Institute of Information Security offers a creative international
environment for top-level international research in Germany's high-tech
region.

The successful candidate should have a Ph.D. (or should be very close to
completion thereof) in Computer Science, Mathematics, Information
Security, or a related field. We value strong analytical skills.
Knowledge in one or more of the following fields is an asset:

 - Formal Methods (Verification, Theorem Proving, F*, Type Checking, etc.)
 - Security Protocol Analysis
 - Web Security

Knowledge of German is not required.

The University of Stuttgart is an equal opportunity employer.
Applications from women are strongly encouraged. Severely challenged
persons will be given preference in case of equal qualifications.

To apply, please send email with subject "Application: Postdoc Position"
and a single PDF file containing the following documents to
ralf.kuest...@sec.uni-stuttgart.de:
* Cover letter (explaining your scientific background and your
motivation to apply)
* Curriculum Vitae
* List of publications
* Copies of transcripts and certificates (Bachelor, Master, PhD)
* Names of at least two references

The deadline for applications is

July 4th, 2021

Late applications will be considered until the position is filled.

See https://sec.uni-stuttgart.de/ for more information about the institute.

See https://www.sec.uni-stuttgart.de/institute/job-openings/ for the
official job announcement.

For further information please contact: Prof. Dr. Ralf Küsters,
ralf.kuest...@sec.uni-stuttgart.de.

-- 
Prof. Dr. Ralf Küsters
Institute of Information Security - SEC
University of Stuttgart
Universitätsstraße 38
D-70569 Stuttgart
Germany
https://sec.uni-stuttgart.de
Phone: +49 (0) 711 685 88283