[TYPES/announce] 2 Ph.D positions on Formal Methods for Rule-based agent safety and concurrent system analysis (U. of Oslo), 15. April

[Martin Steffen]

	   __________________________________________________

		TWO PH.D POSITIONS IN METHODS FOR SECURITY ANALYSIS FOR
    	        AUTONOMOUS AGENTS / CONCURRENT SYSTEMS

			deadline: 15. April 2016

                Dept. of Computer Science, Univeristy of Oslo
		Group of Precise Modelling and Analysis (PMA)

	   __________________________________________________


  There are *two Ph.D positions* available at the group of ``Precise
  modelling and analysis'', generally in the field for rule-based analyzing
  security properties in agent systems resp. for concurrent and distributed
  programs.



---------------------------------------------------------------------------------
  Be aware that when you apply it is important to clearly mark which
  position(s) you are interested in.

  upload link for applying:  http://uio.easycruit.com/vacancy/1597233/64290?iso=no
-----------------------------------------------------------------------------

   Short description of the 2 positions below, more extensive project
   descriptions are  linked in under

      http://www.mn.uio.no/ifi/english/research/groups/pma/news/news-positions-phd-2016-html

   which contains also more details about work-conditions, general rules for applying. 
   required documentation and other side conditions.

======================================

1. Position: ``Safety of autonomous agents'' position
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  The project is about method and tools to assure the safety of autonomous
  information agents. Technically, the project will use and develop
  rule-based and goal based systems and where the desired behavior of such
  agents are described by /safety contracts/. The goals of the thesis are
  to develop

  - /formalisms/ specifying such goals and contracts,
  - /algorithms/ to verify the consistency of such rules and
    synthesizing a rule system to control agents
  - A prototype implementing such agents.

  The project is done in collaboration with the industrial partner
  /Tellu/, and will be using the rule-based framework /SmartTracker/.


2. Position: ``Analysis of non-functional properties in concurrent systems''
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  The project is concerned with formal methods and tools for analyzing
  non-functional properties in concurrent and multi-core programs. The
  candidate will work on program analysis and modelling techniques to
  ensure robust and predictable program execution- The project will use
  and develop /formal methods/, i.e., methods on rigorous semantical
  foundation which allow to reason mathematically about the consequences
  of system designs.  Since static and dynamic analysis techniques have
  complementary strengths (and weaknesses) concerning precision,
  computational overhead, etc. the project will aim at combining
  them. Techniques we plan to use include constraint solving, advanced
  flow analysis, and type-based techniques.


Specific qualifications
=========================

  The applicant is required to hold a Master's degree or equivalent in
  /computer science/ and should have good analytical and programming
  skills. The ideal candidate has background in (some of) the following
  areas of system security and formal methods and program analysis:
  software verification, validation, rule-based reasoning, monitoring and
  testing, semantics, including knowledge of tools in that field.

  Besides technical skills, we are looking for a curious, ambitious
  candidate who is highly motivated to do research and contribute to the
  work done at our group. Good communication skills in both oral and
  written English are expected. We strongly encourage that the
  application is accompanied by a short cover letter explaining shortly
  how the applicant's background and education fits to the goals and
  requirements of this project.