[TYPES] Researcher Position in Formal Methods available at ITC-irst

[NuSMV Recruit]

[Apologies for multiple copies.
 Please forward this message to potentially interested people]

                         RESEARCHER POSITION

                 Automated Reasoning Systems Division
                               ITC-irst
                                Trento
                                Italy

The Automated Reasoning Systems Division (SRA) at ITC-irst is seeking
a researcher to join the team of the PROSYD project. The position
lasts three years and is already open. Monthly salaries vary depending
on age, qualification, and experience.

The PROSYD Project
==================

The Prosyd project -- Property-Based System Design -- is a Specific
Target Research Project sponsored by the European Commission,
Information Society Technologies under the 6th Framework Program. The
consortium includes IBM Haifa Research labs, Infineon, ST
Microelectronics, Weizman Institute of Science, Technical University
of Graz, Verimag and Accelera and ITC-irst (http://www.prosyd.org).

The goal of the PROSYD project is to establish a standard, integrated
property-based paradigm for the design of electronic systems. This
paradigm will integrate and unify the many phases of system
development, including requirement definition, design, implementation,
and verification, into one coherent design flow, building on the
property specification language PSL/Sugar (http//www.pslsugar.org),
which has been recently selected as a basis for an IEEE standard.

The prime deliverable of the PROSYD project will be a reference
methodology and a set of coherent PSL/Sugar-based tools for
property-based system design. Using these tools, an experimental
evaluation activity will demonstrate a significant improvement in
design productivity, as well as an increase in the quality of the
finished product (i.e. reduction of design flaws that make it through
the verification phase).

The role of ITC-irst in the project is twofold. On one side, the
objective is to develop advanced techniques and tools for requirement
analysis, synthesis, and verification. On the other, the NuSMV model
checker (http://nusmv.irst.itc.it) will be extended to deal with
PSL/Sugar specifications.

Description of Activity
=======================
The researcher will be part of the PROSYD team at ITC-irst. The
activity will include design and implementation of new algorithms and
functionalities, their integration into the NuSMV model checker, and
the preparation of project deliverables.

Important research objectives include:

. development of novel techniques for property exploration and
 assurance, aiming to help a designer in finding a complete
 description of the design intent. These techniques will allow to
 identify inconsistencies in specifications as well as cases of
 underspecification.

. development of new algorithms for the efficient static and dynamic
 verification of PSL/Sugar properties using both BDD-based and
 SAT-based engines. Moreover, techniques for error localization
 within the circuit will also be analyzed to simplify the elimination
 of bugs.

. development of techniques for the automatic logic synthesis of
 circuits according to a property based specification for rapid
 design prototyping and for the generation of suitable environment
 for the verification/simulation of circuit components.

. investigation of the applicability of an extended satisfiability
 solver, able to analize boolean combination of propositional
 variables and mathematical constraints. This will enable to reason
 natively at word-level, thus avoiding the potential blow up
 associated with booleanization.

ITC-IRST
========
The Center for Scientific and Technological Research (ITC-irst) is a
public research center of the Autonomous Province of Trento, Italy,
and was founded in 1976. For nearly three decades, the Center has been
conducting research in the areas of Information Technologies,
Microsystems, and Physical Chemistry of Surfaces and Interfaces. 
Today, ITC-irst is an internationally recognized research center with
a budget of 20 million euros. The Center's applied and basic research
activities aim at resolving real-word problems, driven by the need for
technological innovation in society and industry. In addition, the
Center carries out its mission by disseminating and publishing
results, and transferring technology to companies and public entities.
The center has five divisions and two applied units.

The Automated Reasoning Systems (SRA) division of ITC-irst currently
consists of about 80 people. The members of SRA have been actively
working in the field of formal verification since 1990, in the
development of techniques and tools for automated deduction and model
checking. SRA has been active in the development of NuSMV, an open
architecture for model checking, and of bounded model checking
techniques based on decision procedures for propositional
satisfiability (SAT). Model checking techniques have been applied to
the design and verification of safety critical systems, in particular
in the field of railways, avionics, and industrial control.

For more information on the SRA division of ITC-irst, see
http://sra.itc.it/.

Candidate Requirements
======================

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

Background and/or previous experiences in the areas of formal
verification, boolean reasoning, deduction systems, hardware
description languages, requirements engineering, are desired.

Applications
============
Please send your applications via email to:

 nusmv-recruit at itc.it

using 'PROSYD Researcher: application' as subject, and including a
statement of interest and a CV. PostScript, PDF, or plain text formats
are strongly encouraged. Please use the above address also for further
inquiries.