[SMT-LIB] PHD position on SAT/SMT applications to requirement engineering in Trento

[Roberto Sebastiani]

---------------------------------------------------------------------------
    [[[ We apologize if you receive multiple copies of this message ]]]
---------------------------------------------------------------------------

--------------------------------------------------------------
PLEASE FORWARD THIS EMAIL TO WHOEVER YOU MAY THINK INTERESTED.
--------------------------------------------------------------

========================================================================

Call for one PhD position in ICT on "Application of SAT- and SMT-based
optimization algorithms to requirement engineering" at Dept. of Computer
Science & Engineering, University of Trento, Italy.

Advisors: Prof. John Mylopoulos and Prof. Roberto Sebastiani
http://disi.unitn.it/users/john.mylopoulos
http://disi.unitn.it/~rseba
========================================================================

ELIGIBILITY CRITERIA: Candidates are required to have a master -- or
equivalent -- degree in Computer Science, Computer Engineering or
Mathematics, or to obtain it withing November 1st 2011.
 
The ideal candidates should have a good background in logic and in
software engineering. A background knowledge in Propositional
Satisfiability (SAT), Satisfiablity Modulo Theory (SMT), Automated
Reasoning, Knowledge Representation & Reasoning or Formal Methods
would be very-positively evaluated.

All the positions are covered by a scholarship, amounting roughly to
51,000 Euros over the three years. Substantial extra funding is
available for participation in international conferences, schools, and
workshops.

DESCRIPTION: Over the past decade, logic-based goal-oriented
requirements modeling languages have been used in Computer Science in
order to represent software requirements, business objectives and
design qualities. Such models extend traditional AI planning
techniques for representing goals by allowing for partially defined
and possibly inconsistent goals. In past work by the proposers,
a framework for reasoning with such goal models have been proposed. 

The goal af the PhD project is to investigate and implement novel
automated reasoning procedures --or to adapt existing ones-- for
efficiently solving requirements problems expressed as goal models,
for optimizing the solutions according to required criteria and, since
requirements evolve with time, to minimize the effort of finding new
solutions and maximizing the reuse of old solutions.  In particular, a
significant effort will be devoted to investigate and adapt SAT- and
SMT-based algorithms for finding optimal solutions to parameterized
goal models.

HOW TO APPLY: Interested candidates should inquire for further
 information and/or apply by sending email to
 roberto.sebastiani at disi.unitn.it

Applications should contain a statement of interest, with a Curriculum
Vitae, and three reference persons. PDF format is strongly encouraged.

Emails will be automatically processed and should have as subject:

       'PHD ON LUCRETIUS PROJECT' 

INFORMAL ENQUIRIES ARE ENCOURAGED. You can get in touch with Prof. Roberto
Sebastiani (roberto.sebastiani at disi.unitn.it, +39.0461.281514),
in order to have a better understanding of possible research
activities and the formal application details.

FUNDING: The position is funded by the project “Lucretius: Foundations
for Software Evolution", thanks to an ERC (European Research Council)
advanced grant awarded to Prof. John Mylopoulos (2011-2016). The
positions is within the Software Engineering and Formal Methods group,
Department of Information Engineering and Computer Science
(http://www.disi.unitn.it) and the ICT Doctoral School of the
Department (http://ict.unitn.it) of the University of Trento, Trento,
Italy.