[Prev][Next][Index][Thread]

Opening positions for young researchers in Trento

[Please forward this message to potentially interested people.]

                 Young Visiting Researchers Positions on the
                            CALCULEMUS Project
                               on the topic
             "Combination of Boolean and Mathematical Reasoning"

                    Automated Reasoning Systems Division
                                ITC-irst	
                              Trento, Italy


The Automated Reasoning Systems Division (SRA) at ITC-irst advertises
the opening of Pre- and Post-doctoral positions for young researchers
to work on CALCULEMUS, a project funded by the TMR initiative (Training
and Mobility of Researchers) of the European Community, to carry out
research on combination of boolean and mathematical reasoning. The
positions are available immediately, up to the end of the project
(end of August 2004). The duration of the appointments is negotiable.
Monthly salaries vary depending on age, qualification, and experience,
up to a maximum of 2.100 EU and 3.200 EU for Pre- and Post-Doctoral
positions, respectively.

The CALCULEMUS Project
======================
The CALCULEMUS project is funded by the European Community under the
TMR initiative (Training and Mobility of Researchers) of the Fifth
Framework Programme.  The scientific and technological goal of the
network is the design of a new generation of computer algebra systems,
deduction systems, and computer-aided verification tools based on the
integration of the deduction and the computational power of Deduction
Systems and Computer Algebra Systems respectively.  The objectives of
the network are: the design of a new generation of mathematical
software systems and computer-aided verification tools; the training
of young researchers in the broad field of mechanical reasoning and
formal methods; the dissemination and exploitation of the results both
in industry and in academia; the cross-fertilization and amalgamation
of the automated theorem proving (ATP/DS), computer algebra (CAS),
term rewriting systems (TRS), interactive proof development
systems(ITP) and software engineering (SE) research communities. The
network consists of 9 member institutions from 6 different countries.

For more information on CALCULEMUS, see http://www.eurice.de/calculemus/.

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

Description of Research
=======================
The impressive advance in the efficiency of boolean solving techniques
(SAT) has brought large previously intractable problems at the reach
of state-of-the-art solvers.  As a consequence, some hard real-world
problems have been successfully solved by encoding them into SAT.
Unfortunately, simple boolean expressions are not expressive enough
for representing many real-world problems.  On the other hand,
mathematical solvers, like computer-algebra systems or constraint
solvers, cannot handle efficiently problems involving heavy boolean
search, or do not handle them at all.

The MathSAT solver, developed at ITC-irst in cooperation with the
University of Trento, is a framework for integrating a
state-of-the-art SAT solver for propositional logic together with
efficient solvers for different classes of mathematical theories.
The efficiency of MathSAT is due both to the tight integration of the
boolean and mathematical solving subroutines, and to the layered
structure of the mathematical decider, which is organized into levels
dealing with subclasses of formulas of increasing complexity. The
solver has been used to address verification problems in different
domains, e.g., temporal systems, timed and hybrid systems. The
approach extends the Bounded Model Checking (BMC) technique for the
verification of timed systems, and is based on reducing a BMC problem
to the satisfiability of a mathematical formula.

The appointed candidates are expected to perform both research on the
theoretical foundations of the integration of boolean and mathematical
reasoning and to contribute to the development and implementation of
the MathSAT tool. Further directions of research which will be
addressed are optimization and improvements of the MathSAT tool, and
extension of the underlying mathematical theories to include, e.g.,
real and integer linear programming, non-linear programming,
uninterpreted functions.  Verification of RTL circuit designs and of
hybrid systems are foreseen as possible applications fields.

Candidate Requirements
======================
The candidate must be a national of an EU Member State or an
Associated State, or have resided in an EU Member State for at least
five years immediately prior to the appointment. He/she must not be an
Italian citizen, and must not have carried out his/her normal
activities in Italy for more than 12 of the 24 months prior to the
appointment.  He/she must be aged 35 or less at the time of the
appointment.  Candidates must be holders of a doctoral degree or of a
degree that would qualify them to embark on a doctoral degree.
For more information on the EU FP5 regulations, see
http://www.cordis.lu/fp5/management/particip/v-gfpbox4.htm.

The ideal candidate should have a background in the area of boolean
and mathematical reasoning, computer algebra and deduction systems,
very good programming skills, a strong commitment to research
excellence, and the ability to work in a collaborative environment.

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

         Marco Bozzano
         ITC-irst
         Via Sommarive, 18
         Povo, 38050, Trento, Italy
         bozzano@irst.itc.it

Email submission of PostScript, PDF, or plain text is preferable.
Please use the above address also for further inquiries.

==============================================================================
   Marco Bozzano, ITC-IRST
   Via Sommarive 18, Povo, 38050 Trento (Italy)
   http://sra.itc.it/people/bozzano/
==============================================================================