[TYPES/announce] 2 PhD positions in Formal Methods for Cloud Computing in Oslo

[Einar Broch Johnsen]

2 PhD positions combining formal methods, static analysis, and semantics with cloud computing and reflection, are available at the Department of Informatics, University of Oslo. The two PhD fellows will join an international research team on formal methods for virtualized systems and cloud computing. The positions are part of the project CUMULUS: Semantics-based Analyses for Cloud-Aware Computing funded by the Research Council of Norway.

Cloud computing is rapidly becoming the infrastructure of choice for compute- and data-intensive systems, offering pay-as-you-go elastic resource capacity as well as agility to quickly and flexibly deploy new applications. Virtualization technology makes elastic amounts of resources available to a software service; for example, the processing capacity allocated to a service may be dynamically adapted to the needs of the service. Cloud-aware computing refers to a new way of developing applications for cloud deployment, designed for high availability and fine-grained scalability on metered resources. Current trends in cloud computing, such as self-managed software using container technology and Docker, are primary targets for the outcomes of the CUMULUS project.

Our main goal is to reason about a cloud-aware application's resource usage and quality of service by means of static techniques, at design time. Cloud-awareness enables an application to negotiate its own quality of service and opens for dynamic and fine-grained resource management. The project will develop a formal foundation for cloud-aware computing and use this foundation to develop static analysis techniques based on executable models of virtualized systems. The techniques will be used to verify quantitative assertions about the high-level quality of service and low-level resource requirements of cloud-aware applications, for example, the trade-offs between an application's response time and resource usage when the application scales. The choice of techniques will be decided together with the PhD fellows.

The ideal candidate should have an interest in (some of) the following topics:  formal methods, semantics, deductive verification, proof systems, type systems, cost analysis, performance analysis, and tool development.

Deadline: June 1, 2015
More information: http://uio.easycruit.com/vacancy/1374721/64290