Doctoral Student Positions in Information and Communication Technologies on the research project

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

are available at the International Doctorate School in Information and Communication Technologies 
(http://www.ict.unitn.it/) of the University of Trento, Italy, under the joint supervision of

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 Research Program
   DISI, University of Trento,
   via Sommarive 14, I-38123 Povo, Trento, Italy
   http://disi.unitn.it/~rseba/.

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 (SE&FM) Research Program, at Department of 
Information Engineering and Computer Science(DISI) of University of Trento.

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 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.

Ph.D. courses will start in Autumn 2012, and the thesis must be completed in three or four years. 
People enrolled Ph.D. courses are expected to move to Trento, and will receive monetary support 
during phases of their activity.

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

The ideal candidate should have an MS or equivalent degree in computer science, mathematics or 
electronic engineering, and combine solid theoretical background and excellent software development
skills (in particular C/C++).

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

Background knowledge and/or previous experience in the following areas (in order of preference), 
though not mandatory, will be considered very favorably:
- Satisfiability Modulo Theory (SMT)
- Propositional Satisfiability (SAT)
- Model Checking
- Automated Reasoning
- Constraint Solving and Optimization
- Embedded Systems Design Languages (e.g. Verilog, VHDL)

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

Interested candidates should inquire for further information and/or apply by sending email to 
wolf-recruit@disi.unitn.it

Applications should contain a statement of interest, with a Curriculum Vitae, and three reference 
persons. PDF format is strongly encouraged.

Emails will be automatically processed and should have

        'PHD ON WOLF PROJECT'

as subject.

Contact Person
==============

Prof. ROBERTO SEBASTIANI
   Software Engineering & Formal Methods Research Program
   DISI, University of Trento,
   via Sommarive 14, I-38100 Povo, Trento, Italy
   http://disi.unitn.it/~rseba/.
   mailto: rseba[at]disi[dot]unitn[dot]it

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 Research Program at DISI 
============================================================

The SW Engineering & Formal Methods 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.

* Advanced Model Checking Techniques for Formal Verification of
   hardware, embedded critical software, and hybrid systems.

* Applications of Propositional Satisfiability (SAT) to various
   domains.

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.