PROGRAMMER POSITIONS in the NuSMV DEVELOPMENT TEAM

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

          PROGRAMMER POSITIONS in the NuSMV DEVELOPMENT TEAM

	       Automated Reasoning Systems Division
                               ITC-irst
                               Trento
                                Italy

The Automated Reasoning Systems Division (SRA) at ITC-irst is seeking
two young programmers to join the development team of the NuSMV model
checker. Monthly salaries vary depending on age, qualification, and
experience. The positions are available from January to December
2004. Young, talented candidates will have the possibility to apply
for a Ph.D. position on Formal Verification and NuSMV, starting in
2005, at the International Ph.D school at the University of Trento,
sponsored by ITC-irst.

NuSMV
=====
NuSMV is a reimplementation and extension of SMV, the first model
checker based on BDDs. NuSMV is a joint project among several
universities (the Carnegie Mellon University, the University of Genova
and the University of Trento). It has been designed to be an open
architecture for model checking, which can be reliably used for the
verification of industrial designs, as a core for custom verification
tools, and as a test-bed for formal verification techniques. The
current version of NuSMV combines classical BDD-based symbolic
techniques with SAT-based techniques. It supports for past temporal
operators and for strong fairness in LTL and it is integrated with
the ZChaff SAT solver.

NuSMV is freely distributed under LGPL license as an Open Source
project. Since its release, NuSMV has been downloaded in a wide number
of institutions, and is used in academia as research tool and in
industry as a back-end for several verification tools.

For more information on NuSMV, see http://nusmv.irst.itc.it/

Description of Activity
=======================
The activity will include design and implementation of new algorithms
and functionalities, performance profiling and optimization, and
experimental analysis/comparison.

Important objectives include the extension of NuSMV in the following
directions:

. management of PSL/Sugar, the new IEEE standard language for property
  specification. This will be part of an ongoing project with several
  industrial partners aiming to spread the use of the PSL standard
  language both in academia and in industry. For more information on
  PSL/Sugar, see http://www.pslsugar.org/.

. verification of timed systems, hybrid systems, and RTL designs,
  based on the use of extended Boolean-Mathematical solvers (MathSAT).

. development of a script language to allow for an easier interaction
  with the system and to allow for the rapid definition and
  experimentation of new search strategies.

. development of a GUI for simplifying the usage of the system. In
  particular the objective would be to have a graphical editor for SMV
  models, and a tool to graphically show counterexamples.



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 50 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 excellent programming skills, the
ability to work in a collaborative environment, and a strong
commitment to achieving assigned objectives. 

Background and/or previous experiences in the areas of formal
verification, boolean reasoning, deduction systems, hardware
description languages, design of hardware/embedded systems, are
preferable requisites.

Fresh graduates who might be interested in evaluating the possibility
of a Ph.D. are particularly encouraged to apply.


Applications << PHD PROGRAM >> 
============

The International Graduate School in Information and Communication
Technologies is organized by the Department of Information and
Communication Technology (DIT) of the University of Trento in
collaboration with other Research Partners like e.g. ITC-irst.

The educational offer and research opportunities are directed towards
the acquisition of skills required for research and development at
universities, public or private research institutes, and industry. A
Faculty of internationally recognized Italian and foreign professors,
is responsible for the educational activities and take part in the
organization of the doctoral program. The program has a minimum length
of three years and consists of courses concentrated mainly during the
first year, while the third is dedicated to work in research.

The ICT graduate school also combines research with integration both
in industry and technology transfer. The research topics are
theoretical and applied and the dissertations cover the continuum
between innovative applications and theoretical research. The
incorporation of industry guarantees the practical value of the
research, while the University guarantees the innovative aspects as
well as the necessary scientific background. This collaboration is
also demonstrated by the research grants covered by research projects
and other partners.

For information regarding the ICT Ph.D. program at the University of
Trento, please see http://ict.unitn.it/.

Applications
============
To apply, please send a statement of interest and a CV by e-mail to:

         NuSMV Development Team 
         ITC-irst
         Via Sommarive, 18
         Povo, 38050, Trento, Italy

         [email protected]

Email submission of PostScript, PDF, or plain text is preferable.
Please use the above address also for further inquiries.
--------------------------------------------------------------------------
mercury-ads mailing list
post:  [email protected]
administrative address: [email protected]
unsubscribe: Address: [email protected] Message: unsubscribe
subscribe:   Address: [email protected] Message: subscribe
--------------------------------------------------------------------------