PhDs and PostDoc on Cloud and Event-based Programming, Security (École des Mines de Nantes, France)

ASCOLA is a joint team (a so-called INRIA project-team) of the Computer Science Departement of École des Mines de Nantes and INRIA’s research center in Rennes. ASCOLA is also a team of Laboratoire Informatique de Nantes Atlantique (LINA, UMR CNRS 6241).

The research team addresses the general problem of evolving software by developing concepts, languages, implementations and tools for building software architectures based on components and aspects. Its long term goal is the development of new abstractions for the programming of software architectures, their representation in terms of expressive programming languages and their correct and efficient implementation.

We will mainly pursue the following objectives:

  • New concepts, language support and tools for distributed applications, in particular, in order to cope with their crosscutting concerns, such as distribution itself, transactional behavior, security.
  • A model that seamlessly integrates components and aspects, in particularly by means of a notion of interfaces that allows to decouple concrete components and aspects while supporting the analysis and enforcement of composition properties in such a hybrid setting.
  • Investigate the relationship between domain-specific languages (DSLs), aspect languages and composition langages. We intend to harness similarities between these language classes for the development of more general language design/implementation techniques in order to provide new support for the transformational development of correct and efficient implementations from high-level programming abstractions.
  • Study of the foundations of AOP and their compositional properties by means of formal semantics for aspects (and components) as well as new corresponding analysis, verification and validation techniques.

We will apply and thus validate our results in the context of (real-world) applications in the domains of enterprise information systems, service-oriented architectures (middleware, business components), cluster and grid programming, as well as pervasive systems.

Full offers here.

Posted in PhD, PostDoc | Comments Off

PostDocs in Computer Security (University of Luxembourg, Luxembourg)

The University of Luxembourg seeks to hire two outstanding post-doctoral researchers at its Interdisciplinary Centre for Security, Reliability and Trust (SnT). One of the positions is within the ApSIA research group led by Prof. Dr. P.Y. Ryan and the second within the SaToSS research group led by Prof. Dr. Sjouke Mauw.

The post-docs will be working on formalizing and applying formal reasoning to real-world security problems and trust issues. The research topics will include: security protocols, security modeling, formal methods for security, socio-technical aspects of security, risk management, privacy, verification, etc. The positions will be partially funded by the national research project STAST: Socio-Technical Analysis of Security and Trust, which aims to develop strategies and tools to detect and prevent attacks involving human, physical and digital elements.

Deadline for applications: May 30, 2013

Continue reading

Posted in PostDoc | Comments Off

PostDocs in (Usable) Security (Carnegie Mellon University, PA, United States)

We invite applications for two postdoc positions in CyLab at Carnegie Mellon University.

  • Position 1: Research on static and run-time mechanisms for enforcing security properties, including information-flow properties, on distributed systems such as mobile operating platforms and browsers. A strong background in programming languages is required. Knowledge of static analysis of Java or Java bytecode is a plus.
  • Position 2: Research on the privacy and usability aspects of online identity management. Experience with user interface design or running user studies is required. Knowledge of OAuth or Shibboleth is a plus.

Applicants must have received their PhD, or completed the requirements for their PhD, when the appointment begins. The positions are for one year, optionally extended to two. Both positions are available immediately; we would like to fill them by the end of the summer. Interested candidates should send their CV, research statement, and the names of three people who can be asked for letters of reference to Lujo Bauer <lbauer(at)cmu.edu>.

Posted in PostDoc | Comments Off

PostDoc in Algebraic and Geometric Modelling (Inria Méditerranée, Sophia Antipolis, France)

A post-doctoral position is available at GALAAD, Inria Méditerranée, Sophia Antipolis, France on “Algebraic-Geometric Computation for Manufacturing Applications”.

Application deadline: June 30th, 2013

Continue reading

Posted in PostDoc | Comments Off

PhD in Programming Language Verification (TU Delft, Netherlands)

The Department of Software and Computer Technology of TU Delft has a four year PhD position in Programming Language Verification in the NWO VICI project of Eelco Visser: “The Language Designer’s Workbench. Automating the Verification of Language Definitions”

The objective of the project is to unify work on semantics engineering and mechanized meta-theory with work on language engineering and language workbenches in order to support language designers in the creation of sound language designs. The Language Designer’s Workbench will provide declarative meta-languages to enable language designers to build high quality compilers and IDEs, while also verifying consistency properties of their language definitions. We will build on our previous work on the Spoofax Language Workbench and integrate work on compiler certification from the semantics engineering community.

The grant provides funding for five researchers at PhD and postdoc level. The focus of this first position is on proof engineering for verification of programming languages. But candidates interested in all aspects of the project are invited to apply. The candidate should have a strong background in programming languages research and a demonstrable interest in one or more of the following topics: type systems, type inference algorithms, program analysis, program transformation, compiler construction, theorem proving and proof assistants, verification of language definitions or compilers,
mechanized meta-theory.

For more information about the position including application instructions see this page.

To meet the early application deadline please apply at the page above before June 15 2013. Submissions received after June 15 will be also considered until the position has been filled.

Posted in PhD | Comments Off

PostDoc on Formally-verified analyzers and Floating-point Arithmetic (Inria Saclay, France)

A postdoctoral position is available within the TOCCATA team, a computer science group between Inria Saclay Île-de-France and LRI (UMR 8623 CNRS, University Paris-Sud 11). The position is funded by the ANR VERASCO research project, which investigates the formal verification of static analyzers and compilers.

The position is available starting September 2013 (with some flexibility on the starting date). Funding is available for 23 months and provides a net salary of around 2100 euros/month and standard benefits such as health insurance and social coverage. There are no teaching responsibilities.

Continue reading

Posted in PostDoc | Comments Off

PhD on Mixing Meta-Modeling and Data-Mining for Explicit Modeling of User Traces, Digital Footprints and Online Reputation (Université de Haute Alsace, France)

Meta-modeling is a branch of software engineering concerned with analysis and synthesis of models (descriptions of real world phenomena). The overall goal of data-mining is to extract information from a data sets and transform it into understandable structures for further use.

The scientific objective of this PhD thesis proposal is to investigate how meta-modeling and data-mining might complement themselves.

Application deadline: June 15th, 2013

Continue reading

Posted in PhD | Comments Off

PhD on Parallel Hybrid Metaheuristics on GPU (Université de Haute Alsace, France)

Context

The design of efficient methods for combinatorial optimization is a key issue for many industrial sectors (automotive, aerospace, broadcasting, etc.). Indeed, more and more efficient heuristics and exact methods have been proposed in recent years, enabling the resolution of many difficult problems.

Metaheuristics, such as evolutionary algorithms, particle swarm optimization and ant colony optimization, have been successfully used to solve many hard problems. It is an interesting approach to tackle high-dimensional problems. In the literature, a large and well-diversified set of metaheuristics has been proposed over the years, enabling the resolution of a wide range of problems. To take advantage of this diversity, hybrid metaheuristics have been proposed. In this new class of algorithms, a smart combination of different optimization methods is used. Such hybridizations can be used to take advantage of strengths from different algorithms. Several examples in the literature show that hybrid metaheuristics can provide a more robust and efficient problem-solving, especially for real-world and large-scale problems.

However, this kind of hybridizations is mainly achieved statically and the parameter setting is performed experimentally. To overcome this limitation, we first need to define a proper set of hybridization parameters (how to combine two approaches, when to instantiate a particular approach, etc.). We wish through this thesis to answer these questions, which can help in the design of hybrid metaheuristics, and lead in term to advanced adaptive hybrid metaheuristics (using dynamic and adaptive hybridization).

Recently, graphics processing units (GPU) have emerged as a new popular support for massively parallel computing, mainly thanks to the publication of the CUDA development toolkit. The algorithms developed during this thesis will exploit a GPU cluster (a computer cluster in which each node is equipped with a GPU), through the use of GPGPU. This cluster provides the significant computing power required by these algorithms, especially if they are used to solve problems that require high computational capabilities.

Objective

Development of a library of massively parallel hybrid metaheuristics for single-objective/multi-objective optimization.

Application deadline: June 15th, 2013

Continue reading

Posted in PhD | Comments Off

PhD on Future Filesystems (University of Leicester, United Kingdom)

We seek strong candidates for a Microsoft PhD studentship on “verified filesystems“. The PhD scholarship is fully funded for three years. The project will be supervised by Tom Ridge at the Department of Computer Science, University of Leicester, in collaboration with Andrew Kennedy at Microsoft Research Cambridge.

Project description

Filesystems are extremely important. Users depend on filesystems to store their files whenever they hit “save”. Businesses rely on databases to store their data safely, and these databases in turn rely on the filesystem.

Modern filesystems are designed to satisfy many complicated requirements. As a result, implementations are beset with problems. The implementation code is extremely complex, and almost inevitably contains bugs. These bugs can and do lead to data corruption and loss. Development time is very lengthy. Testing is also very lengthy and costly, and does not guarantee to eliminate all bugs. It is often unclear to application developers what guarantees a filesystem provides, so that it becomes extremely difficult to write correct applications for a given filesystem, let alone applications that are portable across different filesystems.

In this project, we aim to tackle these problems by applying formal methods techniques. We will specify the behaviour of existing filesystems using higher-order logic (supported by the HOL4 theorem prover). Further, we will implement a filesystem, and verify functional correctness of the implementation with respect to the specification. We are particularly interested in the behaviour of filesystems when the host crashes. The project involves theoretical aspects (for example, we are interested in understanding the dependencies that arise when different filesystem operations execute; the project will also involve extensive proofs, both informal and mechanized) but is focused on applications of theory to real-world systems.

Application deadline: June 2nd 2013

Continue reading

Posted in PhD | Comments Off

Postdoctoral positions in Computer Science (LIX, Saclay, France)

LIX, the Laboratory for Computer Science at the Ecole Polytechnique, France, is inviting applications for its 2013-2014 LIX-Qualcomm Postdoctoral Fellowship for research in computer science.

Application deadline: Friday May 31, 2013.

Continue reading

Posted in PostDoc | Comments Off