[TYPES] MathSAT: PhD positions at ICT-Trento

[Alessandro Cimatti]

[[[ Apologies for mutiple copies of this message ]]]

---------------------------------------------------------------------
|                                                                   |
|		     Ph.D. Positions Available on		    |
|								    |
|	     Decision Procedures for Formal Verification	    |
|								    |
|	       at the International Doctorate School on		    |
|	      Information and Communication Technologies	    |
|		     University of Trento, Italy		    |
|								    |
|		      Firm deadline: July 11th, 2005.		    |
|								    |
---------------------------------------------------------------------

The MathSAT team at ITC-irst and at University of Trento is seeking
candidates for two Ph.D. positions at the International Doctorate
School in Information and Communication Technologies (ICT) of the
University of Trento, Italy.

The activity will be carried out within the MathSAT project, and will
aim at the design and development of decision procedures and their
application to formal verification.

Presentation and Inquiries
==========================

Candidates interested in the above positions should introduce
themselves and inquire for further information by sending email to:

	   mathsat-recruit at itc.it

Please use 'MATHSAT PHD' as subject, and include a statement of
interest and a CV. PostScript, PDF, or plain text formats are
encouraged.

Application to the ICT School
=============================

Full details are available from http://www.ict.unitn.it/

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

The ideal candidate should have a MS or equivalent (in either computer
science, mathematics, electronic engineering or similar topics), and
combine solid theoretical background and software development skills.

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

Background knowledge and/or previous experience in the areas of formal
verification, boolean reasoning, constaint solving, deduction systems,
hardware description languages, though not mandatory, will be
considered favourably.

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.

Related Projects
================

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 activity of the selected candidates will be related to the the
ORCHID project (Enhanced Formal Checkers for RTL Circuit Designs).
The goal of the ORCHID project 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.

Contact Persons
===============

* Alessandro Cimatti
  mailto:cimatti at itc.it
  http://sra.itc.it/people/cimatti/

* Roberto Sebastiani
  mailto:roberto.sebastiani at dit.unitn.it
  http://www.dit.unitn.it/~rseba/