[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
We are looking for suitable candidates in various projects and on different levels. For details on the projects see below. PhD researchers (4 years) --------------- (note that these are fully paid positions, not studentships) - 1 PhD on Graphs for the Abstract Interpretation of Languages (GRAIL) - 1 PhD on Multi-Core Model Checking (MCMC) - 1 PhD on Symbolic Translation of Stochastic Processes (STOP) Postdoctoral researchers ------------------------ - 1 Postdoc (1 year) in Graphs for Software Language Definition (GRASLAND) - 1 Postdoc (1.5 year) in INtegrated European Signalling System (INESS) (possibly with an extension to 3 years) - 1 Postdoc (3 years) in Quantitative System Properties in Model-Driven-Design of Embedded Systems (QUASIMODO) Technical assistants -------------------- - 1 Technical Assistant (3 years) for the Laboratory on Interoperability of Small Tools (LIST) Deadline for all applications: 18 April 2008 Project descriptions ==================== GRAIL (PhD researcher, vacancy number 08/075) ----- As more and more systems in our everyday environment contain major software parts, and we are depending on such systems more and more (we are counting on them), the importance of the dependability of the embedded software is increasing. Unfortunately, there are still very few generally applicable methods for software verification, i.e., ensuring its correct functioning under all circumstances. Reasons for this are, on the one hand, the degree of expertise necessary for existing verification methods, and on the other, their poor embedding in the average software development trajectory. An important practical objection is, moreover, that current verification methods typically assume the existence of a sufficiently detailed and precise model of system behaviour. In practice such models hardly ever exist, and the time and expertise to construct them is missing. Examples of methods that are being used widely in practice are therefore typing and testing, neither of which necessarily depends on the pre-existence of models. In this project we investigate a new way of automatically verifying software on the basis of code, without assuming a predefined model. The technique used is static analysis, a general principle that encompasses typing; the new aspect is the use of graph transformations to capture the effect of the software. Graphs offer a natural model for the behaviour of dynamic software systems, and at the same time offer the basis for a generic form of static analysis, which can be driven by the properties to be verified. For further information, please contact Arend Rensink [EMAIL PROTECTED] or consult the full project description (http://fmt.cs.utwente.nl/grail) MCMC (PhD researcher, vacancy number 08/076) ---- The goal of this project is to develop model checkers that exploit the computing power of clusters of computers, GRIDs, multi-core machines, and their heterogeneous combination. We aim at the development and understanding of new distributed and parallel algorithms, and we want to build a high-quality tool. We will consider branching and temporal logics, parity games, including some quantitative extensions. For further information, please contact Jaco van de Pol [EMAIL PROTECTED] STOP (PhD researcher, vacancy number 08/077) ---- The goal of this project is to integrate model checking techniques for languages with rich data types, and languages with probabilistic, stochastic, and timing information. The aim is to identify, study and implement model transformations at the language level, in order to minimize state spaces even before their generation, while preserving functional and quantitative properties. Topics of interest are linearization, static analysis, abstraction, and confluence reduction for languages with data and quantitative information. For further information, please contact Jaco van de Pol [EMAIL PROTECTED] or Joost-Pieter Katoen [EMAIL PROTECTED] GRASLAND (Postdoc, vacancy number 08/078) -------- In the context of the MDA (Model Driven Architecture) methodology for designing maintainable software systems, model transformation is a central concept. Models are used to describe the system in all phases of development and on various levels of abstraction; they are specified in diverse (modelling and programming) software languages (SLs). Model transformations typically introduce concrete, implementation specific details. Such transformations are intended to be correctness preserving: they should not introduce errors or essential changes. This, however, can be guaranteed only if the meaning of the SLs involved is defined with sufficient precision. Unfortunately, this is often lacking: many SLs have a well-defined syntax but only an informal semantics. A primary reason for this is that MDA does not include a general method for easily and consistently defining the subtler aspects of SLs, such as their semantics. The purpose of this project is to define a meta-language in which all aspects of SLs, besides their concrete syntax, can be defined in a consistent manner. As a common formal foundation of this meta-language we propose graphs and graph transformations, which we believe to be powerful enough to capture all relevant SL aspects. This meta-language will enable us to provide semantic definitions of the source and target SLs involved in a given model transformation on a compatible basis; this in turn will enable us to precisely formulate and check the requirement of correctness preservation. We believe these abilities to be essential in realizing the full potential of MDA. For further information, please contact Arend Rensink [EMAIL PROTECTED] or consult the full project description (http://trese.cs.utwente.nl/grasland). INESS (Postdoc, vacancy number 08/079) ----- Today there are over 20 rail signalling and speed-control systems operating in Europe, which are incompatible with each other. This complexity leads to additional costs and increased risk of breakdowns. Promoted by the European Commission and driven by the need for interoperability and harmonisation of safety, the European Rail Traffic Management System (ERTMS) aims to remedy this lack of unification in the signalling and speed control. The INESS project aims at contributing to the above mentioned European initiatives by defining and developing specifications for a new generation of interoperable interlocking systems suitable to be integrated in the ERTMS system to ease the migration. This will enhance the standardisation process and therefore, help increasing the competitiveness of the railway transport. In Twente, you will work on formal specification and validation of requirements on railway signalling systems, and on verifying and testing their design. We promise you a very interesting case study. For further information, please contact Jaco van de Pol [EMAIL PROTECTED] QUASIMODO (Postdoc, vacancy number 08/080) --------- Quasimodo is a European research project funded by the European Commission under the IST framework programme 7 for Information and Communication Technology, ICT. Partners are found in Denmark, Germany, France and The Netherlands. Embedded Systems is the designation for intelligent and smart computer controlled mechanical devices. Today - and even more so in the near future - computers are built into everyday appliances existing anywhere in our surroundings. Examples include laundry-machines, climate control systems, cars, and satellites. It is the combination of mechanics, computer electronic, and an enormous amount of software that makes the devices intelligent, but at the same time so extremely complex that they are difficult to develop. The main goal of Quasimodo is to develop new techniques and tools for model-driven design, analysis, testing and code-generation for advanced embedded systems while ensuring quantitative bounds on resource consumption is a central problem. Within this goal, the effort of the University of Twente will be towards various aspects, such as model checking, controller synthesis, and testing. The postdoc is expected to contribute to the research in one or more of these fields, in close cooperation with the ESI (Embedded Systems Institute) and several industrial partners in the Quasimodo project. For further information, please contact Rom Langerak [EMAIL PROTECTED] or consult the project web site, http://www.quasimodo.aau.dk. LIST (Technical Assistant, vacancy number 08/081) ---- A "small tool" is the type of software tool typically created in the course of a research project, as carried out by a single PhD student. Such tools have a small basis for maintenance and more often than not "die" with the end of the project, without having had a chance of being embedded or tested in a larger, systems engineering context. It is a common observation, recently repeated in the Dutch 3TU computer science assessment, that policy and infrastructure are missing to change this situation. In this project, we propose to set up a framework for the improved integration and maintenance of small tools in the area of formal methods, with the aim of offering such tools better usability, better accessibility and a longer lifespan. This will provide these tools with more chance of proving themselves in practice, and thus help to valorise the effort that went into their creation. The project will be carried out in cooperation with similar efforts at the Technical Universities of Eindhoven and Delft. The task of the technical assistant will initially consist of forging concrete interoperability links between specific (existing) tools. Using the expertise thus built up, the next step is to generalise from this, and to identify and bring together the necessary elements for an integration and maintenance framework. For further information, please contact Arend Rensink [EMAIL PROTECTED] Profile ======= To qualify for any of the PhD positions, you must have an MSc or comparable degree and a good background in formal methods. Expertise in the specific area of the project is considered an advantage. Good English speaking and writing skills are demanded, as well as the willingness to learn Dutch. The candidates will enrol in the PhD programme of the Dutch Research School for Programming Research and Algorithmics (IPA). To qualify for any of the postdoc positions, you must have a PhD degree in a relevant area of formal methods. Good English speaking and writing skills are demanded, as well as the willingness to learn Dutch. Offer ===== A PhD researchership in the Netherlands is a fully paid position, for a period of 4 years. The candidate will receive a gross salary starting at 2000 per month (first year) and reaching 2558 per month (final year), plus an 8% holiday allowance and other benefits. The postdoc positions are for 1 year (GRASLAND), 1.5 years (INESS) and 3 years (QUASIMODO), respectively. Your starting salary is 2802 per month, but may be higher depending on experience, plus an 8% holiday allowance and other benefits. The technical assistant position is for 3 years. Your starting salary is 2802 per month, but may be higher depending on experience, plus an 8% holiday allowance and other benefits. To qualify for the technical assistant position, you must have a BSc degree from a university or polytechnic, practical programming skills, as well as the ability to grasp and abstract problems, and to understand the principles behind formal methods tools. Good English speaking and writing skills are demanded, as well as the willingness to learn Dutch. Experience with software development and maintenance is an advantage. Application =========== You are invited to send your application together with: - A cover letter stating your *specific* interest in the position, indicating also your motivation and qualifications for joining the project. (In the absence of such a cover letter your application will be rejected without notification.) - A full curriculum vitae, including the subject and supervisor of your graduate thesis (in case of a PhD or TA position) or PhD thesis (in case of a postdoc position). - Letters of recommendation or references of at least two scientific staff members. Letters should be sent by email to the relevant contact person, mentioning the vacancy number in the header, with a cc to Ms. Joke Lammerink [EMAIL PROTECTED] : - GRAIL PhD researcher: [EMAIL PROTECTED], vacancy number 08/075 - MCMC PhD researcher: [EMAIL PROTECTED], vacancy number 08/076 - STOP PhD researcher: [EMAIL PROTECTED] and [EMAIL PROTECTED], vacancy number 08/077 - GRASLAND postdoc: [EMAIL PROTECTED], vacancy number 08/078 - INESS postdoc: [EMAIL PROTECTED], vacancy number 08/079 - QUASIMODO postdoc: [EMAIL PROTECTED], vacancy number 08/080 - LIST technical assistant: [EMAIL PROTECTED], vacancy number 08/081 All applications must be received ** at or before 18 April 2008 **