CS为主Logic/math/philosophy相关的positions

The Formal Methods and Tools chair of the University of Twente is looking for suitable candidates for the following positions:

- 1 Postdoc position for 3 years in the EU-ARTEMIS project CHARTER
(Critical and High Assurance Requirements Transformed through Engineering Rigor)

- 1 Technical Assistant position for 3 years in the LaQuSo-project LIST
(Laboratory for the Interoperability of Small Tools)

We first describe these projects and the role of the applicants. Details about
where to apply and what to provide with your application follow at the end of
the mail. For further information contact Arend Rensink (rensink@cs.utwente.nl)

Deadline for applications: 15 January 2009.


CHARTER (3 year postdoc position, vacancy number 08/309)
=======

CHARTER is a European project in which 7 industrial and 3 academic partners work together. The following is en excerpt from the general project description:

Future generations will experience software pervasiveness that can hardly be imagined today. Embedded systems will literally be found everywhere and control almost everything. Human life will depend on software to an inconceivable extent. To protect our society from the resulting severe risks, ever more software will be subject to governmental regulations. Whenever software is deployed in sensitive applications, certification processes will be needed. The costly and time-
consuming procedures employed today to verify new software, for example in the air flight industry, will fail to meet demands of this scale.

CHARTER will ease, accelerate, and cost-reduce the certification of critical embedded systems by melding realtime Java, Model Driven Development, rule-based compilation, and formal verification. This approach, Quality-Embedded Development (QED), will push software certification to a new level and thereby significantly contribute to the safety and security of the upcoming age of an embedded software society.

The role of the University of Twente in this project is to lead the work package in which a tool for certifiable model transformation is developed. This task is to be carried out by the postdoc, in coordination with other work packages, which in fact act as users of the tool. The intended technological basis for the model transformation is graph transformation.

The position is for 3 years. The starting salary is at least 2861 Euro gross per month, but may be higher depending on experience, plus an 8% holiday allowance, an 8,3% end-of-year bonus and a number of additional benefits. Start date of the project is 1 Februari, but a later start is negotiable.

To qualify for this position, you must have a PhD degree in an area related to graph transformation, model transformation, or model-driven software engineering, as well as have a background in formal methods. Good English speaking and writing skills are demanded, as well as the willingness to learn Dutch.


LIST (3 year technical assistant position, 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.

This position is for 3 years. The starting salary is at least 2861 Euro gross per month, but may be higher depending on experience, plus an 8% holiday allowance, an 8,3% end-of-year bonus and a number of additional benefits.

To qualify for the 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.


Information and Application
===========================

More information can be obtained from Arend Rensink (rensink@cs.utwente.nl).

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 may be rejected without
notification.)

- A full curriculum vitae, including the subject and supervisor of your
graduate thesis (for the TA position) or PhD thesis (for the postdoc position).

- Letters of recommendation or references of at least two scientific staff
members.

Applications should be sent by email to Arend Rensink (rensink@cs.utwente.nl), mentioning the vacancy number in the header, with a cc to Ms. Joke Lammerink
(jlammeri@cs.utwente.nl):

- CHARTER postdoc: vacancy number 08/081
- LIST technical assistant: vacancy number 08/309.

All applications must be received ** at or before 15 January 2009 **

Modeling and analysis of security protocols
===========================================

One post-doc position is available in the Department of Computer Science,
Stevens Institute of Technology.

The project is led by Professors Susanne Wetzel and David Naumann.  It involves
development of analytic models and simulations of wireless network protocol
stacks, including both abstract protocol specifications and actual
implementations. We will create techniques and tools that integrate automated
formal methods of exhaustive analysis with guided runtime testing.

The post-doc's primary responsibilities will include: Development of detailed
design models; specification of secrecy, authenticity, and other properties of
the models; static analysis of models and implementations using model-checking,
type-checking, and other techniques; collaboration with other team members on
testing and simulation.

The work will be conducted at Stevens Institute of Technology, in Hoboken, New
Jersey, across the Hudson river from New York City.

Expected skills: (a) PhD in computer science (or equivalent) with a publication
record in security, in particular analysis of security properties of
implementations; (b) familiarity with model-checking, runtime assertion
checking, and type-based static analysis for access control and information flow
policies; and (c) very good written and oral English skills.

The post-doc can start until January 2009, and will last 12 months. Salary will
be competitive based on qualifications and experience. A second year is possible
based on accomplishments and availability of funds.

The application should contain the following (a) a curriculum vitae including a
list of publications and software products as well as statement of research
goals; (b) names and email addresses of two references.

Applications and questions should be sent by email to the address you infer from
this:  postdoc-applications cs DOT stevens DOT edu

Applications received by December 8, 2008 will receive full consideration and
applications may be considered until the position is filled.

Positions are contingent upon completion of the PhD.  Stevens Institute of
Technology is an affirmative action/equal opportunity employer; women, minorities, veterans, and disabled persons are encouraged to apply.

The Formal Methods and Tools chair of the University of Twente is looking for suitable candidates for the following positions:

- 1 Postdoc position for 3 years in the EU-ARTEMIS project CHARTER
(Critical and High Assurance Requirements Transformed through Engineering Rigor)

- 1 Technical Assistant position for 3 years in the LaQuSo-project LIST
(Laboratory for the Interoperability of Small Tools)

We first describe these projects and the role of the applicants. Details about
where to apply and what to provide with your application follow at the end of
the mail. For further information contact Arend Rensink (rensink@cs.utwente.nl)

Deadline for applications: 15 January 2009.


CHARTER (3 year postdoc position, vacancy number 08/309)
=======

CHARTER is a European project in which 7 industrial and 3 academic partners work together. The following is en excerpt from the general project description:

Future generations will experience software pervasiveness that can hardly be imagined today. Embedded systems will literally be found everywhere and control almost everything. Human life will depend on software to an inconceivable extent. To protect our society from the resulting severe risks, ever more software will be subject to governmental regulations. Whenever software is deployed in sensitive applications, certification processes will be needed. The costly and time-
consuming procedures employed today to verify new software, for example in the air flight industry, will fail to meet demands of this scale.

CHARTER will ease, accelerate, and cost-reduce the certification of critical embedded systems by melding realtime Java, Model Driven Development, rule-based compilation, and formal verification. This approach, Quality-Embedded Development (QED), will push software certification to a new level and thereby significantly contribute to the safety and security of the upcoming age of an embedded software society.

The role of the University of Twente in this project is to lead the work package in which a tool for certifiable model transformation is developed. This task is to be carried out by the postdoc, in coordination with other work packages, which in fact act as users of the tool. The intended technological basis for the model transformation is graph transformation.

The position is for 3 years. The starting salary is at least 2861 Euro gross per month, but may be higher depending on experience, plus an 8% holiday allowance, an 8,3% end-of-year bonus and a number of additional benefits. Start date of the project is 1 Februari, but a later start is negotiable.

To qualify for this position, you must have a PhD degree in an area related to graph transformation, model transformation, or model-driven software engineering, as well as have a background in formal methods. Good English speaking and writing skills are demanded, as well as the willingness to learn Dutch.


LIST (3 year technical assistant position, 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.

This position is for 3 years. The starting salary is at least 2861 Euro gross per month, but may be higher depending on experience, plus an 8% holiday allowance, an 8,3% end-of-year bonus and a number of additional benefits.

To qualify for the 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.


Information and Application
===========================

More information can be obtained from Arend Rensink (rensink@cs.utwente.nl).

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 may be rejected without
notification.)

- A full curriculum vitae, including the subject and supervisor of your
graduate thesis (for the TA position) or PhD thesis (for the postdoc position).

- Letters of recommendation or references of at least two scientific staff
members.

Applications should be sent by email to Arend Rensink (rensink@cs.utwente.nl), mentioning the vacancy number in the header, with a cc to Ms. Joke Lammerink
(jlammeri@cs.utwente.nl):

- CHARTER postdoc: vacancy number 08/081
- LIST technical assistant: vacancy number 08/309.

All applications must be received ** at or before 15 January 2009 **

The Distributed and Embedded Systems (DIES) and Information Systems (IS) research groups at the University of Twente

collaborate with a number of industrial partners in the project Value-Based Security Risk Mitigation in Enterprise Networks that are Decentralized (VRIEND). In this project there is a two year PostDoc position available, see:



http://dies.cs.utwente.nl/~pieter/adverts/Vriend_advert.pdf

Posted: December 19, 2008

Doctoral Student Positions in Information and Communication Technologies

on the research project "WORD-LEVEL FORMAL VERIFICATION VIA SMT SOLVING"

are available at the International Doctorate School in Information and
Communication Technologies (http://www.ict.unitn.it/) of the
University of Trento, Italy, under the joint supervision of

Dr. ALESSANDRO CIMATTI,
Embedded Systems Research Unit,
FBK-Irst,
via Sommarive 18, I-38100 Povo, Trento, Italy
http://sra.fbk.eu/people/cimatti/,
Prof. ROBERTO SEBASTIANI
Software Engineering & Formal Methods Research Program
DISI, University of Trento,
via Sommarive 14, I-38100 Povo, Trento, Italy
http://disi.unitn.it/~rseba/.

The research activity will be carried out jointly within the Embedded Systems
(ES) Research Unit of the Center for Scientific and Technological
Research of the Fondazione Bruno Kessler (FBK), Trento, and the
Software Engineering & Formal Methods (SE&FM) Research Program,
at Department of Information Engineering and Computer Science (DISI) of
University of Trento.

The research activity will aim at investigating and developing novel
techniques, methodologies and support tools for Satisfiability Modulo
Theories (SMT) for the verification of WORD-level circuit designs.
This work will be part of the "Word-Level Formal Verification via SMT
Solving" (WOLFLING) project, a three-year custom research project
supported by SRC/GRC (http://grc.src.org/fr/S200802_Call.asp), in
strict collaboration with the Formal Verification Group at Intel, Haifa.

SMT tools will be developed on top of the MathSAT SMT platform
(http://mathsat4.disi.unitn.it), and Formal Verification tools will be
developed on top of the NuSMV Model Checking platform (http://nusmv.fbk.eu).
Both platforms are jointly developed and maintained by ES and SE&FM.

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 excellent 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
(in order of preference), though not mandatory, will be considered
very favorably:
- Satisfiability Modulo Theory (SMT)
- Propositional Satisfiability (SAT)
- Embedded Systems Design Languages (e.g. Verilog, VHDL)
- Symbolic Model Checking
- Automated Reasoning
- Constraint Solving and Optimization

Applications and Inquiries
==========================

Interested candidates should inquire for further information and/or
apply by sending email to Prof. Sebastiani rseba[at]disi[dot]unitn[dot]it.

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

      'PHD ON WOLFLING PROJECT'

as subject.

Contact Person
==============

Prof. ROBERTO SEBASTIANI
Software Engineering & Formal Methods Research Program
DISI, University of Trento,
via Sommarive 14, I-38100 Povo, Trento, Italy
http://disi.unitn.it/~rseba/.
mailto: rseba[at]disi[dot]unitn[dot]it

The Embedded Systems Research Unit at FBK
=========================================

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 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
research, is active in the areas of Information Technology,
Microsystems, and Physical Chemistry of Surfaces and
Interfaces. Today, FBK is an internationally recognized research
institute, collaborating with industries, universities, and public and
private laboratories in Italy and abroad. The institute's applied and
basic research activities aim at resolving real-world problems, driven
by the need for technological innovation in society and industry.

The SW Engineering & Formal Methods Research Program at DISI
============================================================

The SW Engineering & Formal Methods R. P. at DISI currently
consists on 5 faculties, 4 post-docs and 19 PhD students. The
Unit carries out research, tool development and technology transfer in
the fields of Goal-Oriented Requirements Engineering, Agent-oriented
SW engineering, Security, and Formal Methods.

Referring to formal methods, current research directions include:

* Satisfiability Modulo Theory, and its application to the
verification of hardware, embedded critical software, and hybrid
systems.

* Advanced Model Checking Techniques for Formal Verification of
hardware, embedded critical software, and hybrid systems.

* Applications of Propositional Satisfiability (SAT) to various
domains.

The R.P. is part of the Department of Information Engineering and
Computer Science, DISI (http://disi.unitn.it/) of University of Trento.
University of Trento in the latest years has always been rated among the
top-three small&medium-size universities in Italy.
DISI currently consists of 50 faculties, 68 research staff and support
people, 21 postdocs and 146 Doctoral students, plus administrative and
technical staff. DISI covers all the different areas of information
technology (computer science, telecommunications, and electronics)
and their applications. These disciplines above are studied
individually but also with a strong focus on their integration,

Location
========

Trento is a lively town of about 100.000 inhabitants, located 130 km
south of the border between Italy and Austria. It is well known for
the beauty of its mountains and lakes, and it offers the possibility
to practice a wide range of sports. Trento enjoys a rich cultural and
historical heritage, and it is the ideal starting point for day trips
to famous towns such as Venice or Verona, as well as to enjoy great
naturalistic journeys. Detailed information about Trento and its
region can be found at http://www.trentino.to/home/index.html?_lang=en.

3 POSTDOC AND 4 PHD POSITIONS IN SECURITY
                AT THE UNIVERSITY OF LUXEMBOURG

                http://satoss.uni.lu/vacancies/

The University of Luxembourg is looking to strengthen the Security and
Trust of Software Systems (SaToSS) group of its Faculty of Science,
Technology and Communication. Security and reliability is one of the
strategic priorities of the University of Luxembourg. These vacancies
concern the following recently approved projects.

- Assessing the Security of Systems Through Attack and Defense Trees
(1 Postdoc position + 1 PhD student position):

Attack trees are a well-known methodology to describe the possible
security weaknesses of a system. An attack tree basically consists
of a description of an attacker's goals and their refinement into
subgoals. The purpose of this project is to extend, formalize, and
develop the attack tree methodology as to make it a systematic,
fully-fledged, and practical security assessment tool.

- A Formal Approach to Enforced Privacy in e-Services (1 Postdoc
position + 1 PhD student position):

Recently, strong privacy properties in voting such as
receipt-freeness and coercion-resistance were proposed. These strong
notions of privacy, which we will call enforced privacy, actually
capture the essential idea that privacy must be enforced by a system
upon its users. The first aim of this project is to extend enforced
privacy from voting to other domains, such as online auctions,
anonymous communications, healthcare, and digital rights management,
where enforced privacy is a paramount requirement. The second aim of
the project is to develop a domain-independent formal framework in
which enforced privacy properties in different domains can be
captured in a natural, uniform and precise way.

- Secure Decisions Through Managing Trust (1 PhD student position):

In practice security is not a simple yes-no question, because a
decision to engage with a system or agent may depend on one's trust
in the system. In order to make this notion of trust more precise a
wealth of models for the management of trust, reputation and
recommendation has been proposed in literature. The purpose of this
project is to study the relation between these different models,
possibly developing one or more generic models. Formal methods will
be used to define and analyze the different models. Validation of
the models is by exercising a number of small case studies, possibly
supported by semi-automated tools.

- Game-theoretic Approaches to Security (1 Postdoc position + 1 PhD
student position):

The project aims to develop new approaches to the design and
analysis of secure systems based on the observation that the
security of a system can be considered as the result of a game
between a defender and an attacker of the system. This observation
opens up a wealth of analysis methods from the field of game
theory. It is expected that game theoretic approaches have an impact
on the design and analysis of fair-exchange protocols and other
types of security protocols. Research will be conducted on the study
of security attacks and counter-measures to prevent or mitigate such
attacks. The project will focus on the application of non-zero sum
games and games of imperfect information.

-----------------------------------------------------------------
Requirements for the PhD student positions:

- A master's (or equivalent) degree in Computer Science, Mathematics
or a related field, with a strong interest in Security. Knowledge in
Game Theory is an advantage for the fourth project.
- Inquisitiveness, commitment, and a critical attitude.
- Very good written and oral English skills, a working knowledge in
German and/or French is an advantage.

Requirements for the Postdoc positions:

- A PhD in Computer Science, Mathematics, or a related field with
expertise in security. Expertise in game theory is required for the
fourth project.
- A strong publication record.
- Very good written and oral English skills, a working knowledge in
German and/or French is an advantage.

-----------------------------------------------------------------
Application procedure:

The PhD students will be employed for a period of 3 or 4 years (40
hrs/week). The Postdocs will be employed for a period of 3 years (40
hrs/week). Supervision for the first three projects will be done by
Prof. Dr. Sjouke Mauw. The fourth project will be supervised by
Prof. Dr. Leon van der Torre and Prof. Dr. Sjouke Mauw.

Postdocs and PhD students will be appointed by the University of
Luxembourg. The Postdocs shall start on April 1, 2009 (or shortly
after) and the PhD students shall start in the first half of 2009.

The remuneration for the PhD position is around 24.000 EUR/year netto,
and for the Postdoc position between 43.000 and 52.500 EUR/year netto.

Deadline for application is February 20, 2009.

-----------------------------------------------------------------
Information:

For inquiries about the first three projects and its positions, please
contact Prof. Dr. Sjouke Mauw (sjouke.mauw@uni.lu, +352 4666445480).

For inquiries about the fourth project and its positions, please
contact Prof. Dr. Leon van der Torre (leon.vandertorre@uni.lu, +352
4666445261) or Prof. Dr. Sjouke Mauw (sjouke.mauw@uni.lu, +352
4666445480).

The full job descriptions can be obtained from
http://satoss.uni.lu/vacancies/
_____________________________________

10 PhD, PostDoc, and Engineering Positions offered!!

-----------------------------------------------------------------------
| HATS: Highly Adaptable and Trustworthy Software using Formal Models |
-----------------------------------------------------------------------

HATS is a new Integrated Project funded by the European Union, within the
programme "Future and Emerging Technologies" (FET) of the 7th Framework
Programme (subject to contract) starting March 2009.

The project partners from
  Chalmers Technical University, Gothenborg, Sweden
  University of Oslo, Norway
  Royal Institute of Technology, Stockholm, Sweden
  Technical University of Madrid, Spain
  IMDEA Software, Spain
  Technical University of Kaiserslautern, Germany,
  University of Bologna, Italy,
  Centrum voor Wiskunde en Informatica (CWI), Amsterdam, Netherlands
  Norwegian Computer Center, Oslo, Norway
  Fredhopper B.V., Amsterdam, Netherlands
  Fraunhofer Institute for Experimental SE, Kaiserslautern, Germany,
  Katholieke Universiteit Leuven, Belgium
are jointly advertising several 3-5 year PhD, PostDoc, and Engineering
positions.

The goal of HATS is a tool-supported framework and formal methodology
for the development of long-lived and trustworthy software systems.
Specifically, HATS will turn software product family (SWPF) development
into a rigorous approach. The technical core of the project is an Abstract
Behavioral Specification language which will allow precise description
of SWPF features and components and their instances. For further
information see:

                   http://www.hats-project.eu

Topic areas: Applicants should have a background and/or interest in
one of the topics software modeling, modeling and programming
languages, formal methods, verification, language-based security, type
systems, or concurrency theory.

The following positions are offered:

* 2 PhD positions with emphasis on formal modeling and verification at
Chalmers University of Technology. One of the positions is in the EU
project CHARTER which is closely related to HATS. Application
deadline is 9th February 2009. Contact: Prof. Reiner Haehnle. Further
details and information on how to apply at
http://www.chalmers.se/cse/EN/ne ... ns/two-ph-d-student

* A Research Software Engineer at Fredhopper (Amsterdam).
The position will comprise of industrial research on modeling and
verification of key components of Fredhopper's flagship product within the
EU-funded HATS research project.
Fredhopper is the Nr. 1 provider of Search & Merchandising solutions for
online business in Europe and industrial leader in the HATS project.
Apply by 31 January 2009 for the most optimal procedure.
Contact for project information: Dr. Nikolay Diakov.
More information and how to apply at:
http://www.fredhopper.com/public ... h-software-engineer

* 2 PostDoc positions at the University of Bologna.  The emphasis is
  on  formal modeling and verification of the kind of concurrent systems
  studied in Hats using various techniques, including
  behavioural techniques and type systems.
  Application deadline is 31 January
(later applications may also be taken into
account).   Contact: Prof. Davide Sangiorgi, see:
http://www.cs.unibo.it/~sangio/Hats/vacancies.txt

* 3 PhD positions with emphasis on static analysis and security at the
Technical University of Madrid/IMDEA Software. One of the positions
is in the DOVES Spanish project, which is closely related to
HATS. The application deadline is 25 January. Later applications may
also be taken into account if the positions are not
covered. Contact: Prof. German Puebla. Further details and
information on how to apply at
http://clip.dia.fi.upm.es/Job_Openings/hats-doves-phd-grants.html

* 1 PhD and 1 PostDoc position in the area of software modeling and
verification at the University of Kaiserslautern. The emphasis in
the area of software modeling is on semantically founded integration
of behavioral software models, feature-based descriptions of variability
and programs. The emphasis in verification is on modular techniques for
object-oriented models and model refinement. Application deadline
is January 31. Later applications may also be taken into account.
Contact: Prof. A. Poetzsch-Heffter. Further details and information
on how to apply at http://softech.informatik.uni-kl.de/Homepage/OffeneStellen

* Further positions will be announced at this space!


Applicants should have (or expect to have at the start of employment):

* For a PhD position: a good Masters level or excellent Bachelor level
degree (or equivalent) in computer science, mathematics, or a
closely related discipline with knowledge in the areas above. Please
see also individual requirements at each site which can differ.

* For a Postdoc position: a PhD in computer science or mathematics,
preferably with research experience in one of the listed topic
areas.

* For a software engineer position: a Masters or PhD level level degree
(or equivalent) in computer science, mathematics, or a closely
related discipline with good knowledge in the areas of program
verification, automata theory or discrete math. Knowledge of Java
and some programming experience count as a plus.

Regardless of the specific application instructions, each
application should contain:

1) a full CV including letters of recommendation
2) a research statement, indicating the research directions you are
  interesting in and what relevant experience you have
3) transcripts of degree results where available.

To apply, please follow the links given above.
Expressions of interest received by 15 January 2009 are guaranteed
full consideration. Specific application deadlines may vary.
Early contact would be appreciated.

The Laboratory of Model-Driven Engineering for Real-Time, Embedded Systems (LISE) of the LIST Institute at the French Atomic Energy Commission (CEA) is seeking to fill a post-doctoral researcher position with specialization in model-based engineering.

Goal:

First-class candidates are sought for conducting original research in model-based, analysis-aided, multi-criteria optimization of embedded systems. Specifically, the position is for a motivated researcher to work in two European projects in collaboration with large companies from the automotive and transport industries (e.g., Continental, Volvo, Alstom, Thales, EADS, ABB). Among the main activities assigned to this position are to lay the groundwork for integrating model-based design and multiple analytic techniques for evaluating/guaranteeing performance and reliability properties of embedded systems. The thrust of the research will be on the definition of optimized architectural patterns guaranteeing generic properties by-construction, and adapting search strategy algorithms to guarantee correct composition (e.g., deadline-missing, deadlock, and error free) of different architectural solutions of a given design decision problem.

Context:

CEA is one of the foremost technological research organizations in Europe on energy, defense, safety, health and information technologies. In the European context, CEA is committed to play an important role as an industry-driven research institution. Details of the LIST Institute can be found in http://www-list.cea.fr. In the field of model-driven engineering for embedded systems, our laboratory (LISE) has a recognized reputation and has been strongly contributing to the state of the art as a core actor in research and engineering of model-based methods and tools. Its contributions are mainly focused on closing the gap between requirements, architecture design, implementation, and validation and verification activities, as well as in the participation within international normalization activities, particularly as the leaders of the MARTE (UML profile for Modeling and Analyzing Real-Time and Embedded systems) standardization work at OMG (Object Management Group). Industrial application is a core concern at LISE, which is reflected by its strong collaboration with large industries, such as for example with automotive industries to define the AIT-WOODES model-based development methodology (now named ACCORD|UML), and more recently with Airbus to integrate our Eclipse-based Papyrus modeling tool (now an Eclipse Component) and Topcased tools into a common infrastructure for model development.

Applicants:

Applicants should hold a Ph.D. in Computer Science or a related engineering discipline, with a research specialization in model-driven engineering and/or embedded/real-time applications. Preference will be given to candidates who have experience in engineering/quantitative analysis of non-functional properties. The position is funded for a period of one year with the option to extend the period by a half year. English is mandatory, French is a plus, but is not required.

Applicants should submit a Curriculum vita, lists of publications and references to huascar dot espinoza at cea dot fr.

Exploiting the Static Single Assignment form in a tool-chain for the formal verification of Transaction-Level Models (TLM) of Systems-on-a-Chip written in SystemC.


This position is offered in the context of the openTLM project
of the Minalogic Competitiveness pole.

Announce:

http://www-verimag.imag.fr/~maraninx/?breve11


Deadline for applications: February 15th, 2009.




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

Context: Transaction-Level Modeling of Systems-on-a-Chip
--------------------------------------------------------

The Register Transfer Level (RTL) used to be the entry point of the design flow of hardware systems, including systems-on-a-chip (SoCs). However, the simulation environments for such models do not scale up well. Developing and debugging embedded software for these low level models before getting the physical chip from the factory is no longer possible at a reasonable cost. New abstraction levels, such as the Transaction-Level Modeling, have emerged. The TLM approach uses a component-based approach, in which hardware blocks are modules communicating with so-called transactions. The TLM models are used for early development of the embedded software, because the high level of abstraction allows a fast simulation. This new abstraction level requires that SoCs be described in some non-deterministic asynchronous way, with new synchronization mechanisms, quite different from the implicit synchronization of synchronous circuit descriptions.

SystemC is a C++ library used for the description of SoCs at different levels of abstraction, from cycle accurate to purely functional models. It comes with a simulation environment, and is becoming a de facto standard. SystemC offers a set of primitives for the description of parallel activities representing the physical parallelism of the hardware blocks. The TLM level of abstraction can be described with SystemC.


VERIMAG and STMicroelectronics Common Projects
----------------------------------------------

VERIMAG and STMicroelectronics have been working together on TLM-related problems since 2002. The main problems we are looking at are the following:

- How to connect SystemC to formal verification tools; this relies on a front-end for SystemC called PINAPA, and on a semantic extractor able to transform abstract syntax trees of SystemC models into some format suitable for model-checking or abstract interpretation tools. The whole tool-chain is called LusSy.

- How to cover correctly the potential parallelism that is present in a SystemC design, and that is supposed to represent faithfully the physical parallelism of the hardware? Our tool relies on dynamic partial order reduction techniques.

- How to define precisely the nature of the information that should be present in pure functional models (also called TLM-PV, for "programmer’s view") and in timed models (also called TLM-PVT, for "programmer’s view + time")? How to construct a PVT model from a PV one without modifying its functionality, as seen by the developer of the embedded software?

- How to define precisely what a TLM component should be, be it written in SystemC or not?

These questions are being addressed in several projects:
- OpenTLM is a project of the competitiveness pole MINALOGIC in Grenoble
- FoToVP (Formal Tools for the Virtual Prototyping of Embedded Systems) is a French National Project


The LusSy Tool-Chain
--------------------

The LusSy tool-chain (mentioned above) does a succession of transformations on SystemC source code to generate the input format for various model-checkers.

One of the components of this tool-chain is Pinapa, which is the equivalent of a compiler front-end for a programming language, but applied to SystemC (which is indeed a C++ library). Pinapa uses GCC to analyze the C++ part of the code, but adds to the abstract syntax tree (AST) information on dedicated SystemC constructs (like the platform’s architecture, which component is connected to whom, ...), thus allowing the extraction of a formal semantics from a SystemC program.

In the meantime, some interesting works have been carried out (in particular by INRIA Rennes, also known as IRISA, our partner in the FoToVP project) on the use of SSA (for "Static Single Assignment") to perform efficient proofs of imperative code. The SSA form is an intermediate form widely used in compilers since it is the one on which optimization algorithms works best. It has been shown that natural and efficient transformations from SSA to proof engines exist.



Objectives of the Post-Doc
---------------------------

The subject proposed is to introduce the notion of SSA form into the tool-chain LusSy, in particular in the component Pinapa, while improving its flexibility and extensibility. Indeed, Pinapa extracts an abstract syntax tree close to the source language. Applying formal methods with this tree as a starting point is complex and not very efficient. Introducing SSA in the tool would improve this point.

The goal of this post-doc would therefore be to explore the possibilities of introducing an SSA form within Pinapa.

Technically, two ways are possible obtain SSA code from a C++ program: GCC 4.x, which uses an SSA form internally, and (probably better), LLVM which uses SSA in its byte-code.

But the real problem is to identify the SystemC specific constructs, which have already been broken down into simpler constructs in SSA code. For example, when one analyses the code

port.write(42);

we can consider it as a "normal" C++ piece of code, that any C++ front-end can analyze, but Pinapa will recognize it as a SystemC specific construct: it is a write operation on a port, and Pinapa needs to know at least who is connected to this port.


Summary of expected work
------------------------

We expect :
- A method to match SSA code against SystemC constructs. This is the central point of the work.
- the definition of an intermediate format containing the useful information on SystemC. This format must be usable as an entry for verification tools
- A prototype-tool which could become the next version of Pinapa. The tool should be able to read SystemC code and to produce the defined intermediate format.

Point 2 must be achieved in collaboration with a post-doctoral researcher that is currently working on intermediate formats as inputs for verification tools. In addition, we expect a student to work with the candidate on technical solutions (LLVM, gcc, etc.) for point 3.


Required Skills
----------------

The ideal candidate should have a Ph.D degree in computer science, combine solid theoretical background and software development skills, and have some degree of autonomy. Good English speaking and writing skills are required (French is not required). The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives.

In depth previous experience in the following areas is required:
- C++ (some knowledge of SystemC would be appreciated)
- Compilation (architecture of a compiler, SSA form. Knowledge of LLVM would be appreciated).
- Formal languages


Terms of employment
-------------------

A full-time position as a postdoctoral researcher for an initial period of 12 months starting as soon as possible after march 1st, 2009. The position can be extended to 6 more months.

The salary will be min. 2500 EUR and max 3000 EUR gross per month depending on qualifications and experience.


Application
-----------

Send a detailed CV, a list of publications, a list of referees (persons that can recommend you), and a short letter explaining your motivations for this position, by email to:

Florence.Maraninchi@imag.fr,Matthieu.Moy@imag.fr,kevin.marquet@imag.fr

Please include [POSTDOC SOC] in the subject of your mail, and only attach PDF files.

Send your application as soon as possible, and no later than February 15, 2009

Ph.D. Position in Information Flow Security

The School of Computer Science and Communication (CSC) at KTH, the Royal Institute of Technology, in Stockholm announces one Ph.D. student position in theoretical computer science for a project on program analysis for information flow security.

KTH is the largest technical university in Sweden. Education and research cover a broad spectrum within natural sciences and engineering, as well as architecture, industrial engineering and management, urban planning, work science and environmental engineering. There are circa 12,000 full-year undergraduate students, 1,400 postgraduate students and 3,100 employees.

CSC is one of Sweden's most advanced and successful research and education institutions in Information Technology. We work with education and research in Numerical Analysis, Computer Science, Media Technology, Human-Computer Interaction, Speech Technology, Music Acoustics and Languages at KTH and at Stockholm University (SU). For more information see

    * http://www.kth.se/csc?l=en_UK

The Department of Theoretical Computer Science (TCS) offers a strong research environment spanning a wide range of research topics within theoretical computer science including complexity theory, cryptography, language technology, and program logics and analysis.

Information flow security concerns the problem of determining and controlling the information flowing between components of a computer system. Information flow security underpins such basic security concepts as confidentiality and integrity, and is of fundamental importance in computer security. Since the late 90´es substantial progress has been made in identifying basic models for information flow security. Unfortunately, the practical impact of this research has been small. There are a number of reasons for this, including an overly restrictive security model, and an overly restrictive scope that largely ignores, for instance, timing attacks.

The goal of the project is to develop new models that can more precisely constrain applications to allow those information channels that are intended for the application at hand, while disallowing side channels, including timing channels. The security model will be phrased in terms of a new concept of "secure sub-computation", capturing the situation where parts of a computation must be strictly constrained when applied to secret, or high-integrity data, whereas other parts can act freely on public data. The model will be examined from both a theoretical and a practical point of view, in terms of efficient algorithms, implementations on Java bytecode, and experiments.

The project is supervised by Dr Mads Dam

    * http://www.csc.kth.se/~mfd

and will involve interaction with other projects in the group, including the EU FP7 project HATS

    * http://www.hats-project.eu

Qualifications

The applicant is expected to have a strong background and interest in computer science, including subjects such as program logic, program analysis, and semantics.

To address its varied work, KTH aims to employ a diversity of talent and thus welcomes applicants who will add to the variety of the University, especially as concerns its gender structure.
Employment

The Ph.D. position is for a maximum of five years, normally including 20% departmental duties (typically course assistance).

The salary of this position follows the CSC/KTH standard salaries of graduate student positions. The Ph.D. student can be enrolled either at KTH or at Stockholm University. Starting date can be discussed.

Form of employment: Time limited

Start date: According to agreement
Application

The application should contain a letter where the applicant describes himself/herself, his/her qualifications and interests. It should also contain a Curriculum Vitae, grade transcripts, copies of the applicant's Master thesis and/or publications, and names and addresses of three referees.
Applicants about to finish their M.Sc. degrees may be considered for the position.

The application should be sent to:

KTH CSC
att. Susanne Bergman
100 44 Stockholm

    * susanneb@csc.kth.se

Application deadline: 2009-02-13.

Employer's reference number: D-2009-0011
Contact

Queries concerning PhD studies at KTH can be directed to:
Eva-Lena Åkerman, personnel office
Phone: +46 8 790 9106

    * ela@csc.kth.se

Queries concerning the project content can be directed to:
Mads Dam, Dr.
Phone: +46 8 790 6229

    * mfd@kth.se