[Hol-info] Work opportunities for Students/Graduates at Fondazione Bruno Kessler
(Apologies if you have received multiple copies of this announcement) WORK OPPORTUNITY FOR STUDENTS/GRADUATES AT FBK! Ideal candidates for this position are young people with strong computer programming skills and a desire to engage in a path of professional growth in the area of research. We are looking for people willing to work in international teams, attracted by research and innovation, with a spirit of initiative and critical thinking skills. If you are interested in joining our top class Research Units, check out the details below! -- Workplace -- The Embedded Systems (ES) Unit of the Information and Communication Technology Center of the Bruno Kessler Foundation, Trento, Italy consists of about 25 persons, including researchers, Postdoc, PhD 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: * Formal Verification of complex embedded systems leveraging on model checking techniques; * Formal Safety Analysis, based on the integration of traditional (e.g. Fault-tree analysis, FMEA) with symbolic verification techniques. * Contract-based engineering and contract-based formal verification of aerospace systems using model checking techniques; * Contract-based techniques for fault detection, identification relying on model checking techniques; * Formal Requirements Analysis based on techniques for temporal logics (consistency checking, vacuity detection, input determinism, cause-effect analysis, realizability and synthesis); * Model based planning and scheduling for aerospace and robotic (drone) systems, for the management of autonomous vehicles, drones for exploration in critical environment, factory automation, and for process optimizations (with applications in Industry 4.0), leveraging model checking and satisfiability modulo theory techniques; * Model based on-board autonomy for different vehicles (AUV, ROV) using planning and scheduling techniques; * Model based recovery relying on planning and scheduling techniques; * Model-based development of controllers for embedded systems; * Satisfiability Modulo Theory, and its application to planning and scheduling, verification of hardware, embedded critical software, and hybrid systems; * Combination of machine learning and symbolic reasoning for predictive maintenance. More information about the ES Unit is available at https://es.fbk.eu/ -- Job Description -- The Embedded Systems (ES) Unit is looking for junior programmers for software development activities related to the different research, technology transfer, and industrial projects in its current portfolio. In particular, the successful candidate will support the ES-Unitâs researchers in the design and development of the different applications and tools to develop and deploy at different premises within the several projects. The successful candidates are expected to work in collaboration with other researchers, programmers, and students involved in the different projects. -- Job requirements -- The ideal candidate should have: * High school diploma/bachelor degree * Software design and development skills; * Knowledge of at least one of the following programming languages: C++, C, Python, Java; * Hands-on experience with standard software development environments under Unix/Linux and/or MS Windows (TM); * Ability to work in a collaborative environment; * Result orientation and flexibility; * Good communication and relational skills in English. FBK will consider Background knowledge and/or previous hands-on experience in the following areas: model-based development of controllers for embedded systems; Eclipse development platform; Xtext framework; UML and/or SysML; XML; symbolic logic; formal methods (e.g., model checking), planning and scheduling, machine learning and machine learning development environments (e.g. scikit-learn, PyTorch, tensorflow). -- Employment -- Type of contract: fixed term contract (technical profile - L4 CCPL) Working hours: part or full time (depending on internal project needs and candidateâs availability) Start date: January 2019 Duration: December 2019 (with possibility to extend the contract depending on funding) Workplace: Trento - Povo Benefits: flexi-time, company subsidized cafeteria or meal vouchers, internal car park, welcome office support for visa formalities, accommodation, social security, etc., reductions on bank account opening fees,
[Hol-info] Post-doc position in the field of Predictive Maintenance at Fondazione Bruno Kessler
(Apologies if you have received multiple copies of this announcement) A RESEARCHER IN THE FIELD OF PREDICTIVE MAINTENANCE FOR THE EMBEDDED SYSTEMS RESEARCH UNIT (ES) -- Job Description -- The Embedded Systems (ES) Unit has an opening for a PostDoc position in the field of predictive maintenance for industrial applications in the framework of several research and technology transfer projects. The successful candidate will be employed for a period of at least two years (with a trial period of 6 months). He/She will carry out research activities in the field of predictive maintenance applied to the analysis of complex critical designs. The candidate is expected to perform activities related to the following research topics: * Development of techniques and tools for combining data driven and model based reasoning to learn models and/or to improve the quality of the models at the basis of the model based approach to run-time monitoring and predictive maintenance; * Development of novel techniques for combining model based reasoning with machine learning to reduce the learning phase, and to improve the quality of the answer generated by the machine learning algorithms, with applications in predictive maintenance, reliability, availability, maintainability, safety and security of data; * Development of a scalable and generic infrastructure for model based predictive maintenance that will allow for different form of analysis to combine sensor data to infer proper abstract states to drive then machine learning algorithms and/or statistical model checking algorithms in predicting the evolution of a system (e.g. future faults, remaining useful lifetime, â¦). * Development of techniques and tools for the automated synthesis of run-time monitor for diagnosis and prognosis, and techniques and tools for model-based synthesis of drivers connecting application to sensors and enriching sensors with meta-data. The candidate is expected to work in collaboration with other researchers, programmers, and students involved in the project. Moreover, the candidate is expected also to interact with industrial partners and to spend some time at industrial partner premises. -- Job requirements -- The ideal candidate should have: * PhD in computer science, mathematics or electronic engineering (to be completed by mid 2019); * Software development skills (preferably in C, C++, Python or Java); * Ability to carry out an independent research program; * Ability to work in a collaborative environment and deliver in research projects and possibly in industrial projects; * Oral and written proficiency in English Additional requirements: In depth previous experience in at least one of the following areas: * Predictive Maintenance * Machine Learning * Symbolic Model Checking * Solid background in logic * Temporal Logics and Property Specification Languages * Satisfiability Modulo Theory * Formal Specification and Analysis of Architectures -- Employment -- Type of contract: Fixed Term Contract (research profile CCPL) Gross annual salary: about ⬠39.300 Working hours: full time Start date: January 2019 End Date: December 2020 Workplace: Trento - Povo Benefits: flexi-time, company subsidized cafeteria or meal vouchers, internal car park, welcome office support for visa formalities, accommodation, social security, etc., reductions on bank account opening fees, public transportation, sport, language course fees. More info at https://www.welfarefbk.info/ -- Application -- Candidates must submit their application by clicking "Apply online" at the bottom of this page. Please make sure to enclose the following documents with your application (pdf format): * Detailed CV * Cover Letter (explaining your motivation for this specific position) * 3 professional references (e-mails and/or phone numbers) Application deadline: 20th December 2018 Please read our Regulations on the recruitment and selection of fixed-term personnel (effective from October 15, 2018) before completing your application. For further administrative information, please contact the Human Resources Services at j...@fbk.eu For technical inquiries about the position, send an e-mail at es-i...@fbk.eu -- The Embedded System Unit (ES Unit) -- The Embedded Systems Research Unit (ES Unit) of the Information and Communication Technology Center of the Bruno Kessler Foundation (FBK-irst), Trento, Italy consists of about 25
[Hol-info] Post-doc position in the field of Formal Methods at Fondazione Bruno Kessler
(Apologies if you have received multiple copies of this announcement) A RESEARCHER IN THE FIELD OF FORMAL METHODS FOR THE EMBEDDED SYSTEMS RESEARCH UNIT (ES) -- Job Description -- The Embedded Systems (ES) Unit has an opening for a PostDoc position in the field of formal verification for industrial applications with the focus on several research and technology transfer projects. The successful candidate will be employed for a period of at least two years (with a trial period of 6 months). He/She will carry out research activities in the field of formal verification and safety assessment applied to the design and implementation of complex industrial size safety critical systems. The candidate is expected to perform activities related to the following research topics: * Declarative languages for to contract-based design and safety assessment; * Design and implementation of scalable formal verification techniques for the verification of temporal properties, to be applied in industrial settings for the design and verification of complex industrial safety-critical systems (e.g. railway domain, avionic domain); * Design and implementation of formal verification techniques for hybrid systems with non-linear dynamics, to be integrated in standard industrial design and verification environments (e.g. CHESS, SCADE, Matlab-Stateflow-Simulink); * Design and implementation of a contract-based framework for compositional verification of systems based on the properties of components, and of a framework for the automatic synthesis of monitors to ensure that local/global properties are satisfied; * Design and implementation of a contract-based safety assessment framework that will allow for the generation of fault-trees, FMEA tables, and reliability measures in a compositional fashion, leveraging on local component results. The candidate is expected to work in collaboration with other researchers, programmers, and students involved in the project. Moreover, the candidate is expected also to interact with industrial partners and to spend some time at industrial partner premises. -- Job requirements -- The ideal candidate should have: * PhD in computer science, mathematics or electronic engineering (to be completed within mid 2019); * Software development skills (preferably in C, C++, Python or Java); * Ability to carry out an independent research program; * Ability to work in a collaborative environment and deliver in research projects and possibly in industrial projects; * Oral and written proficiency in English Additional requirements: In depth previous experience in at least one of the following areas: * Solid background in logic * Temporal Logics and Property Specification Languages * Contracts and Interface Theories * Formal Specification and Analysis of Architectures and Model Based Reasoning * Formal Model-Based Safety Analysis (e.g., automatic generation of fault trees, reliability metrics) * Symbolic (Software) Model Checking * Satisfiability Modulo Theory -- Employment -- Type of contract: Fixed Term Contract (research profile CCPL) Gross annual salary: about ⬠39.300 Working hours: full time Start date: January 2019 End Date: December 2020 Workplace: Trento - Povo Benefits: flexi-time, company subsidized cafeteria or meal vouchers, internal car park, welcome office support for visa formalities, accommodation, social security, etc., reductions on bank account opening fees, public transportation, sport, language course fees. More info at https://www.welfarefbk.info/ -- Application -- Candidates must submit their application by clicking "Apply online" at the bottom of this page. Please make sure to enclose the following documents with your application (pdf format): * Detailed CV * Cover Letter (explaining your motivation for this specific position) * 3 professional references (e-mails and/or phone numbers) Application deadline: 20th December 2018 Please read our Regulations on the recruitment and selection of fixed-term personnel (effective from October 15, 2018) before completing your application. For further administrative information, please contact the Human Resources Services at j...@fbk.eu For technical inquiries about the position, send an e-mail at es-i...@fbk.eu. -- The Embedded System Unit (ES Unit) -- The Embedded Systems Research Unit (ES Unit) of the Information and Communication Technology Center of the Bruno Kessler Foundation
[Hol-info] Post-doc position in the field of Planning and Scheduling at Fondazione Bruno Kessler
(Apologies if you have received multiple copies of this announcement) A RESEARCHER IN THE FIELD OF PLANNING AND SCHEDULING FOR THE EMBEDDED SYSTEMS RESEARCH UNIT (ES) -- Job Description -- The Embedded System (ES) Unit has an opening for a PostDoc position in the field of planning and scheduling for industrial applications in the framework of several research and technology transfer projects. The successful candidate will be employed for a period of at least two years (with a trial period of 6 months). She/he will carry out research activities in various aspects of planning and scheduling, and architectures for autonomy applied to the design and implementation of adaptive autonomous systems with critical timing, safety and security requirements. The candidate is expected to perform activities related to the following research topics: * Declarative languages to specify planning and scheduling domains, keeping into account controllability, partial observability, timing, and resources issues; * Declarative languages to specify conditional time triggered plans suitable to solve complex planning and scheduling problems; * Design and implementation of scalable planning and scheduling solution techniques for applications in industrial settings to control autonomous vehicles as well as for factory automation; * Design and implementation of formal plan validation techniques to be applied in the planning and scheduling domains, suitable for the verification of conditional time triggered plans; * Design and implementation of autonomy architectures encompassing, deliberation, execution and monitoring and interface with low level controls, both for off-line and on-board deployment; * Design and implementation of scalable techniques to handle and deal with planning and scheduling domains in continuous spaces (e.g. motion and path planning). The candidate is expected to work in collaboration with other researchers, programmers, and students involved in the project. Moreover, the candidate is expected to interact with industrial partners and to spend some time at industrial partner premises. -- Job requirements -- The ideal candidate should have: * PhD in computer science, mathematics or electronic engineering (to be completed by mid 2019); * Software development skills (preferably in C, C++, Python or Java); * Ability to carry out an independent research program; * Ability to work in a collaborative environment and deliver in research and/or industrial projects; * Oral and written proficiency in English. Additional requirements: In depth previous experience in at least one of the following areas: * Planning and Scheduling * Autonomy Architecture * Robotic infrastructures (e.g. ROS) * Solid background in logic, temporal logics and property specification languages * Symbolic Model Checking * Satisfiability Modulo Theory * Formal Specification and Analysis of Architectures * Software Model Checking -- Employment -- Type of contract: Fixed Term Contract (research profile CCPL) Gross annual salary: about Euro 39.300 Working hours: full time Start date: January 2019 End Date: December 2020 Workplace: Trento - Povo Benefits: flexi-time, company subsidized cafeteria or meal vouchers, internal car park, welcome office support for visa formalities, accommodation, social security, etc., reductions on bank account opening fees, public transportation, sport, language course fees. More info at https://www.welfarefbk.info/ -- Application -- Candidates must submit their application by clicking "Apply online" at the bottom of this page. Please make sure to enclose the following documents with your application (pdf format): * Detailed CV * Cover Letter (explaining your motivation for this specific position) * 3 professional references (e-mails and/or phone numbers) Application deadline: 20th December 2018 Please read our Regulations on the recruitment and selection of fixed-term personnel (effective from October 15, 2018) before completing your application. For further administrative information, please contact the Human Resources Services at j...@fbk.eu For technical inquiries about the position, send an e-mail at es-i...@fbk.eu. -- The Embedded System Unit (ES Unit) -- The Embedded Systems Research Unit (ES Unit) of the Information and Communication Technology Center of the Bruno Kessler Foundation (FBK-irst), Trento, Italy consists of about 25 people, including
[Hol-info] CFP: Formal Methods for Intelligent Systems @ ISMIS 2018
[ Apologize for Multiple Copies ] Call for Papers 24th International Symposium on Methodologies for Intelligent Systems ISMIS 2018 Special Session - Formal Methods for Intelligent Systems - October 29 - 31, 2018, St. Raphael Resort, Limassol, Cyprus ISMIS is an established and prestigious conference for exchanging the latest research results in building intelligent systems. Held twice every three years, the conference provides a medium for exchanging scientific research and technological achievements accomplished by the international community. The scope of ISMIS is intended to represent a wide range of topics on applying Artificial Intelligence techniques to areas as diverse as decision support, automated deduction, reasoning, knowledge based systems, machine learning, computer vision, robotics, planning, databases, information retrieval, etc. The focus is on research in intelligent systems. The conference addresses issues involving solutions to problems that are complex to be solved through conventional approaches and that require the simulation of intelligent thought processes, heuristics and applications of knowledge. The integration of these multiple approaches in solving complex problems is of particular importance. ISMIS provides a forum and a means for exchanging information for those interested purely in theory, those interested primarily in implementation, and those interested in specific research and industrial applications. Formal Methods for Intelligent Systems -- Traditionally, Formal Methods have been used as rigorous means to prove correctness and safety of software and hardware systems. They are rooted in logic and reasoning, and aim to provide guarantees that the system is behaving correctly, which is necessary in safety-critical contexts. Suchguarantees can be provided automatically for conventional software/hardware systems using verification technologies such as model checking or theorem proving. However, in several (critical) application domains (e.g. planning and scheduling, machine learning, autonomous controllers synthesis, business processes) the underpinning reasoning techniques do not offer the needed guarantees, and reasoning capabilities necessary to justify safety of the application. The scope of this special session is intended to represent research results and discussions about the application and/or combination of Formal Methods (model checking, theorem proving, mathematical reasoning ...) to solve problems in different areas such as Planning and Scheduling, Machine Learning, Decision Support Systems, Robotics, Autonomy, Business Processes. The session addresses issues involving solutions to problems that will benefit from the adoption of Formal Methods. Examples are for instance guarantee robustness of a plan, or robustness of a (deep) neural, robustness/safety of a decision support system or of a robotic controller or of a business process. Topics. -- This special session aims at bringing together academic and industrial leaders who will present and discuss the results that combine Formal Methods to solve problems in different areas related to Intelligent Systems. The topics include, but not limited to: * Intelligent Information Systems * Autonomic and Evolutionary Computation * Logic for Artificial Intelligence * Knowledge Integration and Aggregation * Intelligent Agent Technology * Intelligent Data Processing and Analytics Paper Submission. -- Authors are invited to submit their manuscripts (maximum 10 pages) electronically in Springer's LNCS/LNAI style. For detailed instructions seethe conferencehomepage (http://cyprusconferences.org/ismis2018/); any necessary information concerning typesetting can be obtained directly from Springer's webpage. All submissions will be subject to review by the ISMIS 2018 program committee in consultation with the special session organizers. Publication. -- The accepted papers will be published in ISMIS 2018 proceedings in Springer's LNAI series. Important Dates. -- * Paper submission: May 10, 2018 * Notification of accept/reject: July 10, 2018 * Camera-Ready: July 31, 2018 * Author Registration Deadline: July 31, 2018 Special Session Chairs. -- Marco Roveri Alberto Griggio Fondazione Bruno Kessler Fondazione Bruno Kessler Trento, Italy, Trento, Italy, rov...@fbk.eu
[Hol-info] SEFM 2017: Call for Workshops
; - Objectives; - Intended Audience; - Possible Relevance to IMBSA and SafeComp; - Information about Previous Events including, where applicable, * a link to the website, * the number of submitted and accepted papers, and * the number of attendees. 3. Workshop Format and Agenda - Intended Paper Format: paper template used (e.g. LNCS), number of pages (for full and, if applicable, short papers), categories of papers (research papers, tool papers, position papers, work-in-progress papers, experimental reports, posters, etc.); - Procedures for Selecting Participants (e.g. review process, personal invitation); - Paper Review Process description, if applicable; - Potential Keynote Speakers; - Intended Workshop Format: number of presentations, planned keynotes, panels, etc.; - Estimated Number of Expected Participants; - Specific Requirements (e.g. equipment, room capacity); - Plans for Dissemination, if any, such as: * SEFM Collocated event LNCS proceedings, * other workshop proceedings, * special issues of journals; - Any Specific Requirement the workshop may have. Workshop proposals should consist of one PDF file using the Springer LNCS style (see http://www.springer.de/comp/lncs/authors.html) and should be submitted by email to sefm17_worksh...@fbk.eu by 31 January 2014. If available, also a preliminary call for papers (list of topics, preliminary PC, deadlines, etc.) can be attached to the proposal. -- WORKSHOP CO-CHAIRS - Antonio Cerone, Nazarbayev University, Astana, Kazakhstan - Marco Roveri, FBK, Trento, Italy For further information, please email to sefm17_worksh...@fbk.eu -- [Apologies for multiple postings] CALL FOR WORKSHOP PROPOSALS - SEFM 2017 15th International Conference on SOFTWARE ENGINEERING AND FORMAL METHODS 6-10 September 2017, Trento, Italy http://sefm17.fbk.eu -- IMPORTANT DATES 31 January 2017 - Workshop proposals submission deadline 17 February 2017 - Notification of workshop approval 4-10 September 2017 - 15th SEFM Conference and Satellite Workshops -- BACKGROUND AND OBJECTIVES The aim of the International conference on Software Engineering and Formal Methods is to bring together practitioners and researchers from academia, industry and government to advance the state of the art in formal methods, to scale up their application in the software industry and to encourage their integration with practical engineering methods. Satellite workshops provide further opportunities for collaborating and exchanging ideas about specific topics of Formal Methods and Software Engineering, from conceptual to practical aspects. Presentations and discussions may be based on preliminary results, recent progress, practical experiences and research proposals, and focus on domain-specific contexts, needs and/or applications, multidisciplinary aspects and communities, coordination between representatives of a technical community and proposed, ongoing or recently completed projects. SEFM 2017 invites prospective workshop organisers to submit their ideas for workshops by 31 of January 2017 at the latest. Workshops should be targeted to research work in the areas of Software Engineering and/or Formal Methods (for a list of topics of interest you may visit the conference website). Prospective workshop organisers are requested to follow the guidelines below and are encouraged to contact the Workshop Co-chairs if any questions arise. -- WORKSHOP ORGANISATION DETAILS SEFM 2017 main conference will be held in Trento, Italy, from Wednesday 6 to Friday 8 September 2017. Satellite events, including workshops, will be held on - Monday 4 - Tuesday 5 September; and - Saturday 9 - Sunday 10 September. During the week 11-15 September there will also be two collocated events: - IMBSA 2017 (Int. Simp. on Model-Based Safety and Assessment); - SafeComp 2015 (Int. Cons. on Computer Safety, Reliability, and Security). Depending on their themes, some workshops may be co-associated with SEFM and IMBSA/SafeComp. In this case they will be held on the weekend 9-10 September. In order to make SEFM workshops appealing for participants, we plan to keep the fares as low as possible, with special fees for a combined registration for both workshops and the main conference. However, precise figures have not been decided yet. We also understand that having a good proceedings publication will attract submissions. For that reason, as we have done starting from 2012, we will organise a joint LNCS proceedings volume for SEFM collocated events. Nevertheless, if you have your own agreements for proceedings or special issue publication, you can maintain them. All accepted workshops would be asked to produce a Webpage and a call
[Hol-info] PostDoc Positions on Planning and Scheduling in the Embedded System Research Unit
(We apologize if you receive multiple copies of this message) == Call ES_PANDS_2017_postdoc == Opening date: December 1, 2016 Closing date: January 16, 2017 A PostDoc position is available in the Embedded Systems Research Unit (ES) at Bruno Kessler Foundation (FBK), Center for Information Technology. FBK is a private research institution based in Trento (Italy) and operating in different scientific fields and disciplines. As such, it has the role of keeping the Autonomous Province of Trento within the mainstream of international research. FBK is made up of seven research centers, whose activities and production are available at http://www.fbk.eu/research-centers. The Embedded Systems Research Unit (ES Unit) of the Information and Communication Technology Center of the Bruno Kessler Foundation (FBK-irst), Trento, Italy consists of about 25 people, including researchers, post-docs, PhD students, Master Students, and programmers. The Unit carries out basic and applied research, tool development and technology transfer in the field of automated planning for different application contexts, and design and verification of embedded systems. Current research directions include: * Model based planning and scheduling for aerospace systems, for the management of autonomous vehicles, for factory automation, and for process optimizations (with applications in Industry 4.0), leveraging model checking and satisfiability modulo theory techniques; * Formal Requirements Analysis based on techniques for temporal logics (consistency checking, vacuity detection, input determinism, cause-effect analysis, realizability and synthesis); * Model-based engineering and formal verification of aerospace systems using model checking techniques; * Model based on-board reasoning systems for autonomous vehicles using planning and scheduling techniques; * Formal Safety Analysis, based on the integration of traditional (e.g. Fault-tree analysis, FMEA) with symbolic verification techniques. * Model based techniques for fault detection, identification relying on model checking techniques; * Model based recovery relying on planning and scheduling techniques; * Satisfiability Modulo Theory, and its application to planning and scheduling, verification of hardware, embedded critical software, and hybrid systems (Verilog, SystemC, C/C++, StateFlow/Simulink); More information about the ES Unit is available at http://es.fbk.eu/ . == Job Description == The ES Unit has an opening for a PostDoc position in the field of planning and scheduling for industrial applications in the framework of several research and technology transfer projects. The successful candidate will be employed for a period of at least two years (with a trial period of 6 months). He/She will carry out research activities in the field of planning and scheduling and architectures for autonomy (planning, scheduling, execution, monitoring) applied to the design and implementation of adaptive systems with critical timing, safety and security requirements. In particular, the activities will focus on: * declarative languages to specify planning and scheduling domains, keeping into account controllability, partial observability, timing, and resources issues; * declarative languages to specify conditional time triggered plans suitable to solve complex planning and scheduling problems; * design and implementation of scalable planning and scheduling solution techniques for applications in industrial settings to control autonomous vehicles as well as for factory automation; * design and implementation of formal validation techniques for validation of planning and scheduling domains, and for the verification of conditional time triggered plans; * design and implementation of autonomy architectures encompassing, deliberation, execution and monitoring and interface with low level controls. The candidate is expected to work in collaboration with other researchers, programmers, and students involved in the project. Required: * PhD in computer science, mathematics or electronic engineering (to be completed within 2017); * Software development skills (preferably in C, C++, Python or Java); * Ability to carry out an independent research program; * Ability to work in a collaborative environment and deliver in research projects and possibly in industrial projects; * Oral and written proficiency in English; Preferred: In depth previous experience in at least one of the following areas: * Planning and Scheduling * Autonomy Architecture * Symbolic Model Checking * Solid background in logic * Temporal Logics and Property Specification Languages * Satisfiability
[Hol-info] PhD Positions in Design and Verification of Embedded Software
[[[ Apologies for multiple copies of this message ]]] Doctoral Student Positions Available Design and Verification of Embedded Software Embedded System Research Unit Fondazione Bruno Kessler (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica) Trento, Italy Deadlines: March 16th, 2011, 13:00 (GTM+1) The Embedded System Research Unit (http://es.fbk.eu) of the Bruno Kessler Foundation, Trento, Italy, is seeking several candidates for Ph.D positions. The Ph.D. studies will be held at the International Doctorate School in Information and Communication Technologies (http://www.ict.unitn.it/) of the University of Trento, Italy. The research activity will be carried out within the Embedded Systems Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler. The research activity will aim at techniques, methodologies and support tools for in the following areas: Formal Requirements Engineering: Often bugs discovered in the code can be traced back to flaws and defects in requirements. This project addresses the problem of providing effective techniques for the elimination of defects in requirements. The approach to Formal Requirements Engineering will be based on techniques for temporal logics (e.g., validation of formal system requirements, requirements refinement and evolution, realizability and synthesis) and the related formal problems (e.g., satisfiability for first-order temporal logic, discretization of hybrid temporal formulas). Verification of Critical Systems: The quality of critical systems must be guaranteed with effective analysis tools. The activity will aim at the development of formal techniques for model-based verification and safety assessment of critical systems, including techniques based on model checking and temporal logics for Fault Tree Analysis (FTA), Failure Model and Effects Analysis (FMEA), Fault Detection, Identification and Recovery (FDIR), Particular Risk Analysis (PRA). The specific research directions will be identified within the fields of formal safety assessment for hybrid systems and for autonomous systems; techniques for finding an optimal installation of components in 3D environments, complying with functional, geometrical and safety constraints; certification of safety critical systems. Intelligent Monitoring: Autonomous systems such as planetary rovers and satellites require the ability to act in unpredictable and hostile environments. The ph.d. study on Intelligent Monitoring will address the problem of identifying hidden parts of the state, and to integrate them within a model based planning and scheduling architecture, based on formal verification techniques. The activities will be part of on-going and future projects sponsored by EU-FP7, EU ARTEMIS-JU, European Space Agency, Microsoft Research, and carried out with major industrial players The selected candidates will be initially enrolled in a stage and, if they pass the selection of the Ph.D. school, they will be enrolled as Ph.D. students. Ph.D. courses will start in Autumn 2008, and the thesis must be completed in three or four years. People enrolled in a stage and subsequent Ph.D. courses are expected to move to Trento, and will receive monetary support during both 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 software development skills. 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, though not mandatory, will be considered favorably: - Symbolic Model Checking, - Propositional Satisfiability, - Satisfiability Modulo Theory, - Constraint Solving and Optimization, - Formal Requirements Analysis, - Software Verification, - Software Synthesis, - Embedded System Design Languages (e.g. Verilog, VHDL, System C, and System Verilog), - Safety Analysis (FTA, FMEA). Applications and Inquiries == Interested candidates should inquire for further information and/or apply by sending email to jobs[at]fbk[dot]eu. 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 'RIF: ES/phd' as subject. NOTE THAT AN APPLICATION TRHOUGH THE UNIVERSITY OF TRENTO WEBSITE IS
[Hol-info] FMICS 2010: Call for Papers (deadline extended)
--- Apologies for multiple copies --- ** * 15th International Workshop on * * Formal Methods for Industrial Critical Systems * * FMICS 2010 * * http://es.fbk.eu/events/fmics2010 * ** * September 20-21, 2010* * Antwerp, Belgium * ** IMPORTANT DATES --- Deadline for abstracts (extended):17 April 2010 Deadline for papers (extended): 25 April 2010 Acceptance notification (extended):7 June 2010 Camera-ready version (extended): 7 July 2010 Workshop: 20-21 September 2010 SCOPE OF THE WORKSHOP - The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops bring together scientists and engineers that are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications. Topics include, but are not restricted to: * Design, specification, code generation and testing based on formal methods. * Methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of complex, distributed, real-time systems and embedded systems. * Verification and validation methods that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues). * Tools for the development of formal design descriptions. * Case studies and experience reports on industrial applications of formal methods, focusing on lessons learned or identification of new research directions. * Impact of the adoption of formal methods on the development process and associated costs. * Application of formal methods in standardization and industrial forums. INVITED SPEAKERS To be announced CO-CHAIRS - Stefan Kowalewski (RWTH-Aachen, Germany) Marco Roveri(FBK-irst, Italy) PROGRAM COMMITTEE --- Aarti Gupta (NEC Labs, US) Andreas Podelski(University of Freiburg, Germany) Andy King (Portcullis Computer Security) Barbara Jobstman(VERIMAG, France) Christophe Joubert (Technical University of Valencia, Spain) Daniel Kroening (ETH Zürich, Switzerland) Diego Latella (CNR/IST Pisa, It) Dino Distefano (Queen Mary, University of London, UK) Francois Pilarski (Airbus, France) Holger Hermanns (Universität des Saarlandes, Germany) Hubert Garavel (INRIA Rhône-Alpes, France) Jaco van de Pol (Universiteit Twente, The Netherlands) Jakob Rehof (Technische Universität Dortmund, Germany) J. José Moreno-Navarro (Universidad Politécnica de Madrid, Spain) Jörg Brauer (RWTH Aachen, Germany) Lubos Brim (Masarykova Univerzita, Czech Republic) Maria Alpuente (Technical University of Valencia, Spain) Marco Roveri(FBK-irst, Italy) Pedro Merino(Universidad de Málaga, Spain) Radu Mateescu (INRIA Rhone-Alpes, France) Stefan Kowalewski (RWTH Aachen, Germany) Stefania Gnesi (ISTI-CNR, Italy) Thierry Lecomte (ClearSy, France) Thomas Kropf(Bosch, Germany) Thomas Santen (Microsoft European Innovation Center) Wan Fokkink (Vrije Universiteit Amsterdam, Netherlands) Wilfried Steiner(TTTech, Austria) ERCIM FMICS WG COORDINATOR -- Alessandro Fantechi (Univ. degli Studi di Firenze and ISTI-CNR, Italy) PAPER SUBMISSIONS - Submissions must be made electronically. Papers should be up to 16 pages in LNCS format, with the names and affiliations of the authors and a clear and informative abstract. Additional details may be included in a clearly marked appendix, which will be read at the discretion of the program committee. All submissions must report on original research. Submitted papers must not have previously appeared in a journal or conference with published proceedings and must not be concurrently submitted to any other peer-reviewed workshop, symposium, conference or archival journal. Any partial overlap with any
[Hol-info] FMICS 2010: Call for Papers
--- Apologies for multiple copies --- ** * 15th International Workshop on * * Formal Methods for Industrial Critical Systems * * FMICS 2010 * * http://es.fbk.eu/events/fmics2010 * ** * September 20-21, 2010* * Antwerp, Belgium * ** IMPORTANT DATES --- Deadline for abstracts: 10 April 2010 Deadline for papers: 18 April 2010 Accept/Reject notification:1 June 2010 Camera-ready version: 1 July 2010 Workshop: 20-21 September 2010 SCOPE OF THE WORKSHOP - The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops bring together scientists and engineers that are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications. Topics include, but are not restricted to: * Design, specification, code generation and testing based on formal methods. * Methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of complex, distributed, real-time systems and embedded systems. * Verification and validation methods that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues). * Tools for the development of formal design descriptions. * Case studies and experience reports on industrial applications of formal methods, focusing on lessons learned or identification of new research directions. * Impact of the adoption of formal methods on the development process and associated costs. * Application of formal methods in standardization and industrial forums. INVITED SPEAKERS To be announced CO-CHAIRS - Stefan Kowalewski (RWTH-Aachen, Germany) Marco Roveri(FBK-irst, Italy) PROGRAM COMMITTEE --- Aarti Gupta (NEC Labs, US) Andreas Podelski(University of Freiburg, Germany) Andy King (Portcullis Computer Security) Barbara Jobstman(VERIMAG, France) Christophe Joubert (Technical University of Valencia, Spain) Daniel Kroening (ETH Zürich, Switzerland) Diego Latella (CNR/IST Pisa, It) Dino Distefano (Queen Mary, University of London, UK) Francois Pilarski (Airbus, France) Holger Hermanns (Universität des Saarlandes, Germany) Hubert Garavel (INRIA Rhône-Alpes, France) Jaco van de Pol (Universiteit Twente, The Netherlands) Jakob Rehof (Technische Universität Dortmund, Germany) J. Jose Moreno-Navarro (Universidad Politécnica de Madrid, Spain) Jorg Brauer (RWTH Aachen, Germany) Lubos Brim (Masarykova Univerzita, Czech Republic) Maria Alpuente (Technical University of Valencia, Spain) Marco Roveri(FBK-irst, Italy) Pedro Merino(Universidad de Málaga, Spain) Radu Mateescu (INRIA Rhone-Alpes, France) Stefan Kowalewski (RWTH Aachen, Germany) Stefania Gnesi (ISTI-CNR, Italy) Thierry Lecomte (ClearSy, France) Thomas Kropf(Bosch, Germany) Thomas Santen (Microsoft European Innovation Center) Wan Fokkink (Vrije Universiteit Amsterdam, Netherlands) Wilfried Steiner(TTTech, Austria) ERCIM FMICS WG COORDINATOR -- Alessandro Fantechi (Univ. degli Studi di Firenze and ISTI-CNR, Italy) PAPER SUBMISSIONS - Submissions must be made electronically. Papers should be up to 16 pages in LNCS format, with the names and affiliations of the authors and a clear and informative abstract. Additional details may be included in a clearly marked appendix, which will be read at the discretion of the program committee. All submissions must report on original research. Submitted papers must not have previously appeared in a journal or conference with published proceedings and must not be concurrently submitted to any other peer-reviewed workshop, symposium, conference or archival journal. Any partial overlap with any
[Hol-info] FMICS 2010: Preliminary Call for Paper
--- Apologies for multiple copies --- ** * 15th International Workshop on * * Formal Methods for Industrial Critical Systems * * FMICS 2010 * * http://es.fbk.eu/events/fmics2010 * ** * September 20-21, 2010* * Antwerp, Belgium * ** IMPORTANT DATES --- Deadline for abstracts: 10 April 2010 Deadline for papers: 18 April 2010 Accept/Reject notification:1 June 2010 Camera-ready version: 1 July 2010 Workshop: 20-21 September 2010 SCOPE OF THE WORKSHOP - The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops bring together scientists and engineers that are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications. Topics include, but are not restricted to: * Design, specification, code generation and testing based on formal methods. * Methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of complex, distributed, real-time systems and embedded systems. * Verification and validation methods that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues). * Tools for the development of formal design descriptions. * Case studies and experience reports on industrial applications of formal methods, focusing on lessons learned or identification of new research directions. * Impact of the adoption of formal methods on the development process and associated costs. * Application of formal methods in standardization and industrial forums. INVITED SPEAKERS To be announced CO-CHAIRS - Stefan Kowalewski (RWTH-Aachen, Germany) Marco Roveri(FBK-irst, Italy) PROGRAM COMMITTEE --- Aarti Gupta (NEC Labs, US) Andreas Podelski(University of Freiburg, Germany) Andy King (Portcullis Computer Security) Barbara Jobstman(VERIMAG, France) Christophe Joubert (Technical University of Valencia, Spain) Daniel Kroening (ETH Zürich, Switzerland) Diego Latella (CNR/IST Pisa, It) Dino Distefano (Queen Mary, University of London, UK) Francois Pilarski (Airbus, France) Holger Hermanns (Universität des Saarlandes, Germany) Hubert Garavel (INRIA Rhône-Alpes, France) Jaco van de Pol (Universiteit Twente, The Netherlands) Jakob Rehof (Technische Universität Dortmund, Germany) J. José Moreno-Navarro (Universidad Politécnica de Madrid, Spain) Jörg Brauer (RWTH Aachen, Germany) Lubos Brim (Masarykova Univerzita, Czech Republic) Marco Roveri(FBK-irst, Italy) Pedro Merino(Universidad de Málaga, Spain) Radu Mateescu (INRIA Rhone-Alpes, France) Stefan Kowalewski (RWTH Aachen, Germany) Stefania Gnesi (ISTI-CNR, Italy) Thierry Lecomte (ClearSy, France) Thomas Kropf(Bosch, Germany) Thomas Santen (Microsoft European Innovation Center) Wan Fokkink (Vrije Universiteit Amsterdam, Netherlands) Wilfried Steiner(TTTech, Austria) ERCIM FMICS WG COORDINATOR -- Alessandro Fantechi (Univ. degli Studi di Firenze and ISTI-CNR, Italy) PAPER SUBMISSIONS - Submissions must be made electronically. Papers should be up to 16 pages in LNCS format, with the names and affiliations of the authors and a clear and informative abstract. Additional details may be included in a clearly marked appendix, which will be read at the discretion of the program committee. All submissions must report on original research. Submitted papers must not have previously appeared in a journal or conference with published proceedings and must not be concurrently submitted to any other peer-reviewed workshop, symposium, conference or archival journal. Any partial overlap with any such published or concurrently submitted paper must be clearly indicated
[Hol-info] PhD Positions at the Embedded System Unit of Fondazione Bruno Kessler
[[[ Apologies for multiple copies of this message ]]] Doctoral Student Positions Available Design and Verification of Embedded Software Embedded Systems Research Unit Fondazione Bruno Kessler (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica) Trento, Italy Posted: November 26, 2008 The Embedded Systems Research Unit (http://es.fbk.eu) of the Bruno Kessler Foundation, Trento, Italy, is seeking several candidates for Ph.D positions. The Ph.D. studies will be held at the International Doctorate School in Information and Communication Technologies (http://www.ict.unitn.it/) of the University of Trento, Italy. The research activity will be carried out within the Embedded Systems Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler. The research activity will aim at techniques, methodologies and support tools for the design and verification of embedded systems. In particular, possible topics will include: - Embedded Software Design and Verification - Formal Requirements Analysis - Design and Verification of Hybrid and Timed systems The selected candidates will be initially enrolled in a stage and, if they pass the selection of the Ph.D. school, they will be enrolled as Ph.D. students. Ph.D. courses will start in Autumn 2009, and the thesis must be completed in three or four years. People enrolled in a stage and subsequent Ph.D. courses are expected to move to Trento, and will receive monetary support during both 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 software development skills. 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, though not mandatory, will be considered favorably: - Symbolic Model Checking - Propositional Satisfiability - Satisfiability Modulo Theory - Constraint Solving and Optimization - Formal Requirements Analysis - Software Verification - Software Synthesis - Embedded Systems Design Languages (e.g. Verilog, VHDL, System C, and System Verilog) - Safety Analysis (FTA, FMEA) Applications and Inquiries == Interested candidates should inquire for further information and/or apply by sending email to jobs[at]fbk[dot]eu. 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 'RIF: ES/phd' as subject. Please note that the positions are already open, and they will be evaluated as soon as they arrive. The Embedded Systems Research Unit = 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 unit develops and maintains several tools: * the NuSMV symbolic model checker (http://nusmv.fbk.eu) * the MathSAT SMT solver (http://mathsat.fbk.eu) * the Formal Safety Analysis Platform FSAP (http://fsap.fbk.eu) * the Requirements Analysis Tool RAT (http://rat.fbk.eu) The unit is currently involved in several research projects, funded by the European Union (FP VI and FP VII), the European Space Agency, the European Railway Agency, as well as in industrial technology transfer projects. The projects aim at applying research results to key application domains such as space, avionics, railways, hardware design and mobile embedded applications. 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
[Hol-info] Positions in the Embedded System Unit of Fondazione Bruno Kessler
[[[ Apologies for multiple copies of this message ]]] Doctoral Student Positions Available Design and Verification of Embedded Software Embedded Systems Research Unit Fondazione Bruno Kessler (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica) Trento, Italy Posted: November 26, 2008 The Embedded Systems Research Unit (http://es.fbk.eu) of the Bruno Kessler Foundation, Trento, Italy, is seeking several candidates for Ph.D positions. The Ph.D. studies will be held at the International Doctorate School in Information and Communication Technologies (http://www.ict.unitn.it/) of the University of Trento, Italy. The research activity will be carried out within the Embedded Systems Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler. The research activity will aim at techniques, methodologies and support tools for the design and verification of embedded systems. In particular, possible topics will include: - Embedded Software Design and Verification - Formal Requirements Analysis - Design and Verification of Hybrid and Timed systems The selected candidates will be initially enrolled in a stage and, if they pass the selection of the Ph.D. school, they will be enrolled as Ph.D. students. Ph.D. courses will start in Autumn 2009, and the thesis must be completed in three or four years. People enrolled in a stage and subsequent Ph.D. courses are expected to move to Trento, and will receive monetary support during both 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 software development skills. 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, though not mandatory, will be considered favorably: - Symbolic Model Checking - Propositional Satisfiability - Satisfiability Modulo Theory - Constraint Solving and Optimization - Formal Requirements Analysis - Software Verification - Software Synthesis - Embedded Systems Design Languages (e.g. Verilog, VHDL, System C, and System Verilog) - Safety Analysis (FTA, FMEA) Applications and Inquiries == Interested candidates should inquire for further information and/or apply by sending email to jobs[at]fbk[dot]eu. 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 'RIF: ES/phd' as subject. Please note that the positions are already open, and they will be evaluated as soon as they arrive. The Embedded Systems Research Unit = 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 unit develops and maintains several tools: * the NuSMV symbolic model checker (http://nusmv.fbk.eu) * the MathSAT SMT solver (http://mathsat.fbk.eu) * the Formal Safety Analysis Platform FSAP (http://fsap.fbk.eu) * the Requirements Analysis Tool RAT (http://rat.fbk.eu) The unit is currently involved in several research projects, funded by the European Union (FP VI and FP VII), the European Space Agency, the European Railway Agency, as well as in industrial technology transfer projects. The projects aim at applying research results to key application domains such as space, avionics, railways, hardware design and mobile embedded applications. 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
