[TYPES] YOUNG RESEARCHER POSITION and PROGRAMMER POSITION on MATHSAT AVAILABLE

[Roberto Sebastiani]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% We apologize if you receive multiple copies of this email.     %%%% 
%%%% Please forward it to whoever might be interested.              %%%%    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


         YOUNG RESEARCHER POSITION and PROGRAMMER POSITION 

The MathSAT team at ITC-irst and at University of Trento is seeking a
young researcher and one/two programmers to join the ORCHID project.
The positions last one year, are renewable for two more years, and are
already open. Monthly salaries vary depending on age, qualification,
and experience.

MathSAT
=======

MathSAT (http://mathsat.itc.it/) is a decision procedure for logic
theories combining boolean propositions with constraints over integer
and real variables, and uninterpreted functions.  It has been applied
in different real-world application domains, ranging from formal
verification of infinite state systems (e.g. timed and hybrid systems)
to planning with resources, equivalence checking and model checking of
RTL hardware designs.  The MathSAT family of deciders is based on the
extension of a DPLL-like propositional satisfiability procedure, used
as an assignment enumerator. MathSAT pioneers a lazy and layered
approach, where propositional reasoning is tightly integrated with
solvers of increasing expressive power, in such a way that more
expensive layers are called less frequently.

The ORCHID Project
==================

Formal methods are widely applied as powerful verification and early
debugging techniques in the development of complex industrial
systems. In particular, formal checking at Register-Transfer Level
(RTL) is currently a fundamental step in the design of hardware
circuits.  Most tools for formal checking, however, work at the
boolean level, which is not expressive enough to capture the abstract,
high level (e.g., structural, word level) information of RTL
designs. Tools for formal checking are thus confronted with problems
which are "flattened" down to boolean level so that a predominant part
of their computational effort is wasted into brute force reasoning at
boolean level.  Thus, the checking process would greatly benefit from
the ability to represent and exploit higher level informations.

The goal of the ORCHID project (Enhanced Formal Checkers for RTL
Circuit Designs) is to investigate enhanced SAT-based techniques for
RTL formal checking and to deliver better verification tools for RTL
designs. These tools will avoid flattening by working directly at a
level of expressivity higher than boolean reasoning, and will be able
to analyze larger scale RTL designs. The results of the research will
be applicable to the extension of any existing formal checkers based
on SAT procedures.

The project is carried on with the external collaboration of the Logic
and Validation Technologies, Intel Architecture Group in Haifa, Israel.

Positions and Applications
==========================

The project has open positions for a young researcher and a programmer.

Applications should be sent via email to:

  mathsat-recruit at itc.it

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

Description of Young Researcher Activity
========================================

The activity of the young researcher will include design and
implementation of new algorithms and functionalities, their
integration into the MathSAT solver, the preparation of project
deliverables. Publication of scientific papers will be a primary
objective.

Important research objectives include:
- improving the efficiency of MathSAT by enriching it with new
  algorithms;  
- extending the expressivity of MathSAT, with new constructs
  (including, e.g., bitwise operators and memories);  
- developing new integration algorithms and/or improving current ones;
- developing and implementing new verification tools using MathSAT as
  a back-end. 

The ideal candidate should have a Ph.D. in either computer science,
mathematics, electronic engineering or similar topics, 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, are desired.  Good skills in programming in
C/C++ and software developing are also desired.

Description of Programmer Activity
==================================

The activity will include the implementation of new algorithms and
functionalities, their integration into the MATHSAT solver,
maintenance, and benchmarking.

We encourage the application from young, talented master students who
may be interested in pursuing a Ph.D. at the International School on
Information and Communication Technologies at the University of
Trento.

The ideal candidates must have very good skills in programming in
C/C++ and software developing, and be able to work in a collaborative
environment, with a strong commitment to achieving assigned
objectives.  Background knowledge and/or previous experience in the
areas of formal verification, boolean reasoning, deduction systems,
hardware description languages, though not mandatory, will be
considered favourably.