[fg-arc] Post-doc position in the field of Formal Methods at Fondazione Bruno Kessler

[Marco Roveri]

(Apologies if you have received multiple copies of this announcement)


A RESEARCHER IN THE FIELD OF FORMAL METHODS FOR THE EMBEDDED SYSTEMS
RESEARCH UNIT (ES)

--------------------------------------------------
Job Description
--------------------------------------------------

The Embedded Systems (ES) Unit has an opening for a PostDoc position
in the field of formal verification for industrial applications with
the focus on several research and technology transfer projects. The
successful candidate will be employed for a period of at least two
years (with a trial period of 6 months). He/She will carry out
research activities in the field of formal verification and safety
assessment applied to the design and implementation of complex
industrial size safety critical systems. The candidate is expected to
perform activities related to the following research topics:

* Declarative languages for to contract-based design and safety
  assessment;
* Design and implementation of scalable formal verification techniques
  for the verification of temporal properties, to be applied in
  industrial settings for the design and verification of complex
  industrial safety-critical systems (e.g. railway domain, avionic
  domain);
* Design and implementation of formal verification techniques for
  hybrid systems with non-linear dynamics, to be integrated in
  standard industrial design and verification environments
  (e.g. CHESS, SCADE, Matlab-Stateflow-Simulink);
* Design and implementation of a contract-based framework for
  compositional verification of systems based on the properties of
  components, and of a framework for the automatic synthesis of
  monitors to ensure that local/global properties are satisfied;
* Design and implementation of a contract-based safety assessment
  framework that will allow for the generation of fault-trees, FMEA
  tables, and reliability measures in a compositional fashion,
  leveraging on local component results.

The candidate is expected to work in collaboration with other
researchers, programmers, and students involved in the
project. Moreover, the candidate is expected also to interact with
industrial partners and to spend some time at industrial partner
premises.

--------------------------------------------------
Job requirements
--------------------------------------------------

The ideal candidate should have:

* PhD in computer science, mathematics or electronic engineering (to
  be completed within mid 2019);
* Software development skills (preferably in C, C++, Python or Java);
* Ability to carry out an independent research program;
* Ability to work in a collaborative environment and deliver in
  research projects and possibly in industrial projects;
* Oral and written proficiency in English

Additional requirements:

In depth previous experience in at least one of the following areas:

* Solid background in logic
* Temporal Logics and Property Specification Languages
* Contracts and Interface Theories
* Formal Specification and Analysis of Architectures and Model Based Reasoning
* Formal Model-Based Safety Analysis (e.g., automatic generation of fault trees, reliability metrics)
* Symbolic (Software) Model Checking
* Satisfiability Modulo Theory


--------------------------------------------------
Employment
--------------------------------------------------

Type of contract: Fixed Term Contract (research profile CCPL)
Gross annual salary: about € 39.300
Working hours: full time
Start date: January 2019
End Date: December 2020
Workplace: Trento - Povo
Benefits: flexi-time, company subsidized cafeteria or meal vouchers,
          internal car park, welcome office support for visa
          formalities, accommodation, social security, etc.,
          reductions on bank account opening fees, public
          transportation, sport, language course fees.

More info at https://www.welfarefbk.info/


--------------------------------------------------
Application
--------------------------------------------------

Candidates must submit their application by clicking "Apply online" at
the bottom of this page. Please make sure to enclose the following
documents with your application (pdf format):

* Detailed CV
* Cover Letter (explaining your motivation for this specific position)
* 3 professional references (e-mails and/or phone numbers)

Application deadline:  20th December 2018


Please read our Regulations on the recruitment and selection of
fixed-term personnel (effective from October 15, 2018) before
completing your application.

For further administrative information, please contact the Human
Resources Services at jobs at fbk.eu

For technical inquiries about the position, send an e-mail at
es-info at fbk.eu.


--------------------------------------------------
The Embedded System Unit (ES Unit)
--------------------------------------------------

The Embedded Systems Research Unit (ES Unit) of the Information and
Communication Technology Center of the Bruno Kessler Foundation
(FBK-irst), Trento, Italy consists of about 25 people, including
researchers, post-docs, PhD students, Master Students, and
programmers. The Unit carries out basic and applied research, tool
development and technology transfer in the field of automated planning
for different application contexts, and design and verification of
embedded systems.

Current research directions include:


* Formal Verification of complex embedded systems using model checking
  techniques;
* Formal Safety Analysis, based on the integration of traditional
  (e.g. Fault-tree analysis, FMEA) with symbolic verification
  techniques;
* Contract-based engineering and contract-based formal verification of
  aerospace systems using model checking techniques;
* Contract-based techniques for fault detection, identification and
  recovery relying on model checking techniques;
* Formal Requirements Analysis based on techniques for temporal logics
  (consistency checking, vacuity detection, input determinism,
  cause-effect analysis, realizability and synthesis);
* Satisfiability Modulo Theory, and its application to planning and
  scheduling, verification of hardware, embedded critical software,
  and hybrid systems (Verilog, SystemC, C/C++, SCADE,
  StateFlow/Simulink);
* Model based planning and scheduling for aerospace and robotic
  (drone) systems, for the management of autonomous vehicles, drones
  for exploration in critical environments, factory automation, and
  for process optimizations (with applications in Industry 4.0),
  leveraging model checking and satisfiability modulo theory
  techniques;
* Model based on-board autonomy for different vehicles (AUV, ROV)
  using planning and scheduling techniques;
* Model based recovery relying on planning and scheduling techniques;
* Combination of machine learning and symbolic reasoning for
  predictive maintenance.

More information about the ES Unit is available at http://es.fbk.eu/.