Postdoc positions in SAT/SMT-based Verification available in Trento

One post-doc position in ICT on the research project "Advanced SMT Techniques for Word-level Formal Verification - (WOLF)"is available in 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 EmbeddedSystems (ES) Research Unit of the Center for Scientific andTechnological Research of the Fondazione Bruno Kessler (FBK), Trento,and the Software Engineering, Formal Methods & Security  ResearchProgram, at Department of Information Engineering and Computer Science(DISI) of University of Trento.Aim and Scope============= The research activity will aim at investigating and developing noveltechniques, methodologies and support tools for Satisfiability ModuloTheories (SMT) for the formal verification of systems.  This work willbe part of the "Advanced SMT Techniques for Word-level FormalVerification - (WOLF)" project, a three-year research projectsupported by SRC/GRC (<http://www.src.org/compete/s201113/>), in strictcollaboration with the Formal Verification Group at Intel, Haifa, andother major HW companies.The ultimate goal of the WOLF project is to provide a comprehensiveSMT package to support effective formal verification of systemsranging from RTL circuits all the way up to high-level hardwaredescription languages (e.g. SystemC) and software. The package will beimplemented on top of the MathSAT SMT platform(<http://mathsat.fbk.eu/>), and provided as an API.Candidate Profile=================The ideal candidate should have an PhD in computer science or relateddiscipline, and combine solid theoretical background and excellentsoftware development skills (in particular C/C++).A solid background knowledge and/or previous experience onSatisfiability Modulo Theory (SMT) and/or Propositional Satisfiability (SAT) is required. Previous experience in the following areas will also be consideredfavourably: Model Checking, Automated Reasoning, Constraint Solvingand Optimization, Embedded Systems Design Languages (e.g. Verilog,VHDL).The candidate should be able to work in a collaborative environment,with a strong committment to reaching research excellence and achievingassigned objectives.Terms and dates===============The position will start as soon as possible, and will have to berenewed yearly, for a maximum of three years.  The expected salarywill range from about 2200 to 2400 euros net income, and the grosswill include previdential (social security) contributions.  Facilitiesfor meals at the local canteen can be provided.Applications and Inquiries==========================Interested candidates should inquire for further information and/orapply by sending email to [wolf-recruit@disi.unitn.it](mailto:wolf-recruit@disi.unitn.it), with subject'POSTDOC ON WOLF PROJECT'. Applications should contain a statement of interest, with a CurriculumVitae, and the names of reference persons. PDF format is stronglyencouraged. It should also indicate an estimated starting date. Contact Persons===============Dr. ALESSANDRO CIMATTI,   Embedded Systems Research Unit,   FBK-Irst,   via Sommarive 18, I-38123 Povo, Trento, Italy  <http://sra.fbk.eu/people/cimatti/>, Prof. ROBERTO SEBASTIANI       Software Engineering, Formal Methods & Security Research Program  DISI, University of Trento,   via Sommarive 14, I-38123 Povo, Trento, Italy  [http://disi.unitn.it/~rseba/](http://disi.unitn.it/%7Erseba/). =======================================================================The Embedded Systems Research Unit at FBK=========================================The Embedded Systems Unit consists of about 15 persons, includingresearchers, post-Doc, Ph.D. students, and programmers. TheUnit carries out research, tool development and technology transfer inthe 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 ofthe Autonomous Province of Trento (Italy), founded in 1976. Theinstitute, through its center for the scientific and technologicalresearch, is active in the areas of Information Technology,Microsystems, and Physical Chemistry of Surfaces andInterfaces. Today, FBK is an internationally recognized researchinstitute, collaborating with industries, universities, and public andprivate laboratories in Italy and abroad. The institute's applied andbasic research activities aim at resolving real-world problems, drivenby the need for technological innovation in society and industry.The SW Engineering, Formal Methods & Security Research Program at DISI======================================================================The SW Engineering, Formal Methods & Security R. P. at DISI currentlyconsists on 5 faculties, various post-docs and PhD students. TheUnit carries out research, tool development and technology transfer inthe fields of Goal-Oriented Requirements Engineering, Agent-orientedSW 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.* Optimization in SMT and its applications.* Advanced Model Checking Techniques for Formal Verification of  hardware, embedded critical software, and hybrid systems.  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 thetop-three small&medium-size; universities in Italy.  DISI currently consists of 50 faculties, 68 research staff and supportpeople, 21 postdocs and 146 Doctoral students, plus administrative andtechnical staff. DISI covers all the different areas of information technology (computer science, telecommunications, and electronics) and their applications. These disciplines above are studiedindividually but also with a strong focus on their integration, Location========Trento is a lively town of about 100.000 inhabitants, located 130 kmsouth of the border between Italy and Austria. It is well known forthe beauty of its mountains and lakes, and it offers the possibilityto practice a wide range of sports. Trento enjoys a rich cultural andhistorical heritage, and it is the ideal starting point for day tripsto famous towns such as Venice or Verona, as well as to enjoy greatnaturalistic journeys. Detailed information about Trento and itsregion can be found at <http://www.trentino.to/home/index.html?_lang=en>.