[FM-India] PHD positions in SAT/SMT-based Verification available in Trento

Sat Feb 23 02:28:24 IST 2013

 From: Roberto Sebastiani <rseba at disi.unitn.it>
 To: fmindia at cmi.ac.in
 Date: Fri, 22 Feb 2013 18:49:34 +0100
 Subject: 

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

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

 Posted: February 22, 2013          

 Doctoral Student Positions in Information and Communication Technologies
 on the research project 

 "Advanced SMT Techniques for Word-level Formal Verification - (WOLF)"

 are available at the International Doctorate School in Information and 
 Communication Technologies (http://www.ict.unitn.it/) of the
 University of Trento, Italy, under the joint supervision of 
 - Alessandro Cimatti, FBK, Trento, and
 - Roberto Sebastiani, DISI, University of Trento.

 The research activity will be carried out jointly within the Embedded
 Systems (ES) Research Unit of the Center for Scientific and
 Technological Research of the Fondazione Bruno Kessler (FBK), Trento,
 and the Software Engineering & Formal Methods (SE&FM) Research
 Program, at Department of Information Engineering and Computer Science
 (DISI) of University of Trento.

 The research activity will aim at investigating and developing novel
 techniques, methodologies and support tools for Satisfiability Modulo
 Theories (SMT) for the formal verification of systems.  This work will
 be part of the "Advanced SMT Techniques for Word-level Formal
 Verification - (WOLF)" project, a three-year research project
 supported by SRC/GRC (http://www.src.org/compete/s201113/), in strict
 collaboration with the Formal Verification Group at Intel, Haifa, and
 other major HW companies.

 The goal of the WOLF project is to provide a comprehensive SMT package
 to support effective formal verification of systems ranging from RTL
 circuits all the way up to high-level hardware description languages
 (e.g. SystemC) and software. The package will be implemented on top of
 the MathSAT.5 SMT platform (http://mathsat.fbk.eu/), and provided as an
 API.

 Ph.D. courses will start in Autumn 2013, and the thesis must be
 completed in three or four years. People enrolled Ph.D. courses are
 expected to move to Trento, and will receive monetary support during
 phases of their activity. 

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

 The ideal candidate should have an MS or equivalent degree in computer
 science, mathematics or electronic engineering, and combine solid
 theoretical background and excellent software development skills
 (in particular C/C++).

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

 Background knowledge and/or previous experience in the following areas 
 (in order of preference), though not mandatory, will be considered
 very favorably:
 - Satisfiability Modulo Theory (SMT)
 - Propositional Satisfiability (SAT)
 - Model Checking
 - Automated Reasoning
 - Constraint Solving and Optimization
 - Embedded Systems Design Languages (e.g. Verilog, VHDL)

 Applications and Inquiries
 ==========================

 Interested candidates should inquire for further information and/or
 apply by sending email to wolf-recruit 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

        'PHD ON WOLF PROJECT' 

 as subject.

 Contact Person
 ==============

 Prof. ROBERTO SEBASTIANI     
   Software Engineering & Formal Methods Research Program
   DISI, University of Trento, 
   via Sommarive 14, I-38100 Povo, Trento, Italy
   http://disi.unitn.it/~rseba/. 
   mailto: rseba[at]disi[dot]unitn[dot]it

 The Embedded Systems Research Unit at FBK
 =========================================

 The Embedded Systems Unit consists of about 15 persons, including
 researchers, post-Doc, Ph.D. students, and programmers. The
 Unit carries out research, tool development and technology transfer in
 the fields of design and verification of embedded systems.

 Current research directions include:

 * Satisfiability Modulo Theory, and its application to the
   verification of hardware, embedded critical software, and hybrid
   systems (Verilog, SystemC, C/C++, StateFlow/Simulink).

 * Formal Requirements Analysis based on techniques for temporal logics
   (consistency checking, vacuity detection, input determinism,
   cause-effect analysis, realizability and synthesis).

 * Formal Safety Analysis, based on the integration of traditional
   techniques (e.g. Fault-tree analysis, FMEA) with symbolic
   verification techniques.

 The Embedded Systems Unit is part of Fondazione Bruno Kessler,
 formerly Istituto Trentino di Cultura, a public research institute of
 the Autonomous Province of Trento (Italy), founded in 1976. The
 institute, through its center for the scientific and technological
 research, is active in the areas of Information Technology,
 Microsystems, and Physical Chemistry of Surfaces and
 Interfaces. Today, FBK is an internationally recognized research
 institute, collaborating with industries, universities, and public and
 private laboratories in Italy and abroad. The institute's applied and
 basic research activities aim at resolving real-world problems, driven
 by the need for technological innovation in society and industry.

 The SW Engineering & Formal Methods Research Program at DISI
 ============================================================

 The SW Engineering & Formal Methods R. P. at DISI currently
 consists on 5 faculties, various post-docs and PhD students. The
 Unit carries out research, tool development and technology transfer in
 the fields of Goal-Oriented Requirements Engineering, Agent-oriented
 SW engineering, Security, and Formal Methods. 

 Referring to formal methods, current research directions include:

 * Satisfiability Modulo Theory, and its application to the
   verification of hardware, embedded critical software, and hybrid
   systems.

 * Advanced Model Checking Techniques for Formal Verification of
   hardware, embedded critical software, and hybrid systems. 

 * Applications of Propositional Satisfiability (SAT) to various
   domains. 

 The R.P. is part of the Department of Information Engineering and 
 Computer Science, DISI (http://disi.unitn.it/) of University of Trento. 
 University of Trento in the latest years has always been rated among the
 top-three small&medium-size universities in Italy.  
 DISI currently consists of 50 faculties, 68 research staff and support
 people, 21 postdocs and 146 Doctoral students, plus administrative and
 technical staff. DISI covers all the different areas of information 
 technology (computer science, telecommunications, and electronics) 
 and their applications. These disciplines above are studied
 individually but also with a strong focus on their integration, 

 Location
 ========

 Trento is a lively town of about 100.000 inhabitants, located 130 km
 south of the border between Italy and Austria. It is well known for
 the beauty of its mountains and lakes, and it offers the possibility
 to practice a wide range of sports. Trento enjoys a rich cultural and
 historical heritage, and it is the ideal starting point for day trips
 to famous towns such as Venice or Verona, as well as to enjoy great
 naturalistic journeys. Detailed information about Trento and its
 region can be found at http://www.trentino.to/home/index.html?_lang=en.