[TYPES/announce] Postdoc positions in SAT/SMT-based Verification available in Trento

[Roberto Sebastiani]

---------------------------------------------------------------------------
    [[[ We apologize if you receive multiple copies of this message ]]]
---------------------------------------------------------------------------

--------------------------------------------------------------
PLEASE FORWARD THIS EMAIL TO WHOEVER YOU MAY THINK INTERESTED.
--------------------------------------------------------------

One post-doc position in ICT on the research project 

"Advanced SMT Techniques for Word-level Formal Verification - (WOLF)"

is available in Trento, Italy, under the joint supervision of 
- Alessandro Cimatti, FBK, Trento, and
- Roberto Sebastiani, DISI, University of Trento.

The research activity will be carried out jointly within the Embedded
Systems (ES) Research Unit of the Center for Scientific and
Technological Research of the Fondazione Bruno Kessler (FBK), Trento,
and the Software Engineering, Formal Methods & Security  Research
Program, at Department of Information Engineering and Computer Science
(DISI) of University of Trento.

Aim and Scope
=============
 
The research activity will aim at investigating and developing novel
techniques, methodologies and support tools for Satisfiability Modulo
Theories (SMT) for the formal verification of systems.  This work will
be part of the "Advanced SMT Techniques for Word-level Formal
Verification - (WOLF)" project, a three-year research project
supported by SRC/GRC (http://www.src.org/compete/s201113/), in strict
collaboration with the Formal Verification Group at Intel, Haifa, and
other major HW companies.

The ultimate goal of the WOLF project is to provide a comprehensive
SMT package to support effective formal verification of systems
ranging from RTL circuits all the way up to high-level hardware
description languages (e.g. SystemC) and software. The package will be
implemented on top of the MathSAT SMT platform
(http://mathsat.fbk.eu/), and provided as an API.

Candidate Profile
=================

The ideal candidate should have an PhD in computer science or related
discipline, and combine solid theoretical background and excellent
software development skills (in particular C/C++).

A solid background knowledge and/or previous experience on
Satisfiability Modulo Theory (SMT) and/or 
Propositional Satisfiability (SAT) is required. 
Previous experience in the following areas will also be considered
favourably: Model Checking, Automated Reasoning, Constraint Solving
and Optimization, Embedded Systems Design Languages (e.g. Verilog,
VHDL).

The candidate should be able to work in a collaborative environment,
with a strong committment to reaching research excellence and achieving
assigned objectives.

Terms and dates
===============

The position will start as soon as possible, and will have to be
renewed yearly, for a maximum of three years.  The expected salary
will range from about 2200 to 2400 euros net income, and the gross
will include previdential (social security) contributions.  Facilities
for meals at the local canteen can be provided.

Applications and Inquiries
==========================

Interested candidates should inquire for further information and/or
apply by sending email to wolf-recruit at disi.unitn.it, with subject
'POSTDOC ON WOLF PROJECT'. 

Applications should contain a statement of interest, with a Curriculum
Vitae, and the names of reference persons. PDF format is strongly
encouraged. It should also indicate an estimated starting date. 

Contact Persons
===============

Dr. ALESSANDRO CIMATTI, 
  Embedded Systems Research Unit, 
  FBK-Irst, 
  via Sommarive 18, I-38123 Povo, Trento, Italy
  http://sra.fbk.eu/people/cimatti/, 

Prof. ROBERTO SEBASTIANI     
  Software Engineering, Formal Methods & Security Research Program
  DISI, University of Trento, 
  via Sommarive 14, I-38123 Povo, Trento, Italy
  http://disi.unitn.it/~rseba/. 


=======================================================================

The Embedded Systems Research Unit at FBK
=========================================

The Embedded Systems Unit consists of about 15 persons, including
researchers, post-Doc, Ph.D. students, and programmers. The
Unit carries out research, tool development and technology transfer in
the fields of design and verification of embedded systems.

Current research directions include:

* Satisfiability Modulo Theory, and its application to the
  verification of hardware, embedded critical software, and hybrid
  systems (Verilog, SystemC, C/C++, StateFlow/Simulink).

* Formal Requirements Analysis based on techniques for temporal logics
  (consistency checking, vacuity detection, input determinism,
  cause-effect analysis, realizability and synthesis).

* Formal Safety Analysis, based on the integration of traditional
  techniques (e.g. Fault-tree analysis, FMEA) with symbolic
  verification techniques.

The Embedded Systems Unit is part of Fondazione Bruno Kessler,
formerly Istituto Trentino di Cultura, a public research institute of
the Autonomous Province of Trento (Italy), founded in 1976. The
institute, through its center for the scientific and technological
research, is active in the areas of Information Technology,
Microsystems, and Physical Chemistry of Surfaces and
Interfaces. Today, FBK is an internationally recognized research
institute, collaborating with industries, universities, and public and
private laboratories in Italy and abroad. The institute's applied and
basic research activities aim at resolving real-world problems, driven
by the need for technological innovation in society and industry.

The SW Engineering, Formal Methods & Security Research Program at DISI
======================================================================

The SW Engineering, Formal Methods & Security R. P. at DISI currently
consists on 5 faculties, various post-docs and PhD students. The
Unit carries out research, tool development and technology transfer in
the fields of Goal-Oriented Requirements Engineering, Agent-oriented
SW engineering, Security, and Formal Methods. 

Referring to formal methods, current research directions include:

* Satisfiability Modulo Theory, and its application to the
  verification of hardware, embedded critical software, and hybrid
  systems.

* Optimization in SMT and its applications.

* Advanced Model Checking Techniques for Formal Verification of
  hardware, embedded critical software, and hybrid systems. 
 
The R.P. is part of the Department of Information Engineering and 
Computer Science, DISI (http://disi.unitn.it/) of University of Trento. 
University of Trento in the latest years has always been rated among the
top-three small&medium-size universities in Italy.  
DISI currently consists of 50 faculties, 68 research staff and support
people, 21 postdocs and 146 Doctoral students, plus administrative and
technical staff. DISI covers all the different areas of information 
technology (computer science, telecommunications, and electronics) 
and their applications. These disciplines above are studied
individually but also with a strong focus on their integration, 

Location
========

Trento is a lively town of about 100.000 inhabitants, located 130 km
south of the border between Italy and Austria. It is well known for
the beauty of its mountains and lakes, and it offers the possibility
to practice a wide range of sports. Trento enjoys a rich cultural and
historical heritage, and it is the ideal starting point for day trips
to famous towns such as Venice or Verona, as well as to enjoy great
naturalistic journeys. Detailed information about Trento and its
region can be found at http://www.trentino.to/home/index.html?_lang=en.