PhD on Graph-Based Abstract Interpretation
PhD position at the University of Twente on Graph-Based Abstract Interpretation To carry out the recently awarded Dutch (NWO) research project entitled "Graphs for Abstract Interpretation of Languages" (GRAIL), we are offering a position for a PhD student (fully funded) for a period of four years.
Deadline for applications: December 15th, 2007
Project start date: January 2008, or as soon thereafter as possible
The Context The project takes place at the Formal Methods and Tools chair of the University of Twente. This chair is part of the Department of Computer Science, one of the largest academic departments for computer science in the Netherlands. Project leader is Dr. Arend Rensink. The Project Graphs for Abstract Interpretation of Languages (GRAIL) 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., the ensurance of its correct functioning under all circumstances. Reasons for this are, one 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 behavior.
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.
The full project proposal can be found at: http://www.cs.utwente.nl/~rensink/projects/grail.pdf
Qualifications You should have a MSc or equivalent degree in computer science or a closely related area, or be able to show that you will receive the degree this year (2007). Familiarity with formal verification, abstract interpretation and/or and graph transformations is considered an advantage. You are expected to cooperate in an internationally oriented research environment. Good English speaking and writing skills are demanded, as well as the willingness to learn Dutch.
You will enroll in the PhD programme of the Dutch Institute for Programming Research and Algorithmics (IPA). Offer The selected candidate will be appointed for a period of 4 years with a gross salary starting at ¤ 1956 per month (first year) and reaching EUR 2502 per month (final year), plus an 8% holiday allowance and other benefits.
Information and Application
You can obtain further information about the positions by enquiring from:
Dr.ir. Arend Rensink,
mailto:rensink@cs.utwente.nl,
tel: +31 (0)53 489 4862
fax: +31 (0)53 489 3247
If you are interested, please send an application by email to the above address, including:
- 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.
- Letters of recommendation or references of at least two scientific staff members.
All applications must be received ** at or before December 15th 2007 ** mention vacancy nr. 07/183.
PhD position at the University of Twente on Graph-Based Abstract Interpretation To carry out the recently awarded Dutch (NWO) research project entitled "Graphs for Abstract Interpretation of Languages" (GRAIL), we are offering a position for a PhD student (fully funded) for a period of four years.
Deadline for applications: December 15th, 2007
Project start date: January 2008, or as soon thereafter as possible
The Context The project takes place at the Formal Methods and Tools chair of the University of Twente. This chair is part of the Department of Computer Science, one of the largest academic departments for computer science in the Netherlands. Project leader is Dr. Arend Rensink. The Project Graphs for Abstract Interpretation of Languages (GRAIL) 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., the ensurance of its correct functioning under all circumstances. Reasons for this are, one 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 behavior.
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.
The full project proposal can be found at: http://www.cs.utwente.nl/~rensink/projects/grail.pdf
Qualifications You should have a MSc or equivalent degree in computer science or a closely related area, or be able to show that you will receive the degree this year (2007). Familiarity with formal verification, abstract interpretation and/or and graph transformations is considered an advantage. You are expected to cooperate in an internationally oriented research environment. Good English speaking and writing skills are demanded, as well as the willingness to learn Dutch.
You will enroll in the PhD programme of the Dutch Institute for Programming Research and Algorithmics (IPA). Offer The selected candidate will be appointed for a period of 4 years with a gross salary starting at ¤ 1956 per month (first year) and reaching EUR 2502 per month (final year), plus an 8% holiday allowance and other benefits.
Information and Application
You can obtain further information about the positions by enquiring from:
Dr.ir. Arend Rensink,
mailto:rensink@cs.utwente.nl,
tel: +31 (0)53 489 4862
fax: +31 (0)53 489 3247
If you are interested, please send an application by email to the above address, including:
- 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.
- Letters of recommendation or references of at least two scientific staff members.
All applications must be received ** at or before December 15th 2007 ** mention vacancy nr. 07/183.
