[SMT-LIB] URGENT: PhD position on Satisfiability-based algorithms for Requirements Engineering

[Roberto Sebastiani]

========================================================================
!!!!!!!!!  URGENT: Submission Deadline: March 16th, 2011    !!!!!!!!!!!! 

Last call for one PhD position in ICT on 
"Satisfiability-based algorithms for Requirements Engineering"
at Dept. of Computer Science & Engineering, University of Trento, Italy.

Advisors: Prof. John Mylopoulos and Prof. Roberto Sebastiani

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

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.

INFORMAL ENQUIRIES ARE ENCOURAGED. Please get in touch with Roberto
Sebastiani (rseba at disi.unitn.it, +39.0461.281514) as soon as possible,
in order to have a better understanding of possible research
activities and the formal application details.

HOW TO APPLY: The positions are included in the "Project Specific
Grants - DISI" of the ICT International Doctoral School, University of
Trento, as reported in the official call published at
http://ict.unitn.it/application.  You must submit a formal application
(by March 16 2011 !) to the ICT School (http://ict.unitn.it/). In the
application, you must mandatorily quote the "Project-specific Grants -
DISI" grant:

"Ontologies and algorithms for requirements engineering"

since failure to do so may result in ineligibility for this position.
Closing date for applications (sharp!) is March 16th, 2011, 1 pm, local time. 

Thus, potentially-interested candidates must:

- URGENTLY (by March 16 2011 !!) submit a formal application
  to the ICT School (http://ict.unitn.it/).

- send their CV (and later three recommendation letters) to
  Roberto Sebastiani (rseba at disi.unitn.it) cc-ing Michela Angeli
  (angeli at disi.unitn.it), and

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.