PhD Position in Programming Language Verification
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 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.
|Starting date||September 1, 2013|
|Area||Software Language Engineering|
|Employer||Department of Software and Computer Technology at TU Delft|
|Contact Person||Eelco Visser|
|Posted||May 1, 2013|
|Apply by||June 15, 2013|
Software Language Design and Engineering
This position is part of the NWO VICI project The Language Designer's Workbench and will be performed within the Software Engineering Research Group under supervision of Dr. Eelco Visser. The mission of our Software Language Design and Engineering team is to enable software engineers to effectively design, implement, and apply domain-specific languages with research in three tracks:
Language engineering: investigate the automatic derivation of efficient, scalable, incremental compilers and usable IDEs from high-level, declarative language definitions
Semantics engineering: investigate the automatic verification of the consistency of language definitions in order to check properties such as type soundness and semantics preservation
Language design: investigate the systematic design of domain-specific software languages with an optimal tradeoff between expressivity, completeness, portability, coverage, and maintainability.
The Language Designer's Workbench
Domain-specific software languages (DSLs) reduce the gap between requirements and implementation through linguistic abstraction by providing notation, analysis, verification, and optimization that are specialized to an application domain. Language workbenches assist language designers with the implementation of languages. However, DSL implementations rarely formally guarantee semantic correctness properties such as type soundness and semantics preservation of transformations, since current language workbenches provide no support for such verification, which leads to intricate errors in language designs that are discovered late.
In the Language Designer's Workbench project, we will work towards new methods and techniques for automating the verification of language definitions. The key innovations are: (1) High-level formalisms for the declarative specification of software languages; (2) Efficient and scalable language parametric algorithms for name resolution, type checking, and program execution; (3) Language parametric test generators that attempt to generate counter examples to the correctness of language definitions; (4) Language parametric proof engineering techniques to support automated verification of language definitions.
The techniques will be integrated in the Spoofax Language Workbench and should enable DSL designers to detect semantic errors at low cost in the early stages of the design process. We will evaluate the techniques by verifying and testing a representative set of language definitions.
The funding of 1.5M Euro from NWO for this project enables us to significantly expand the SLDE team to pursue this research agenda.
The PhD candidate will join a world-leading team in software language engineering to contribute to the objectives of the project. The focus of this particular position is on proof engineering for verification of programming languages. But candidates interested in all aspects of the project are invited to apply.
An enthusiastic PhD student with an MSc degree in Computer Science and a documented interest in doing research. 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.
We are looking for a researcher with an independent mind who is willing to collaborate in our team. It is understood that he or she works on the topics listed above, and contributes to the objectives of the project. Further we ask for good communicative and collaborative skills. The working language of the group is English. Candidates should be prepared to prove their English language skills.
As research outcome we expect publications, (prototype) tools, and a PhD dissertation.
Starting date: September 1st, 2013, or as soon as possible thereafter.
A PhD position for four years (38 hrs/week) in a stimulating scientific environment. Gross salary ranging from EUR 2083 (1st year) tot EUR 2664 (4th year) per month with Holiday allowance (8%) and end-of-year bonus (8.3%). In addition, TU Delft offers an attractive benefits package, including a flexible work week, free high-speed Internet access from home (with a contract of two years or longer), and the option of assembling a customised compensation and benefits package (the 'IKA'). Salary and benefits are in accordance with the Collective Labour Agreement for Dutch Universities.
Further information can be found at the following web pages:
- NWO VICI Grant: The Language Designer's Workbench
- Eelco Visser's homepage
- The Software Engineering Research Group
For more information about this position please contact Eelco Visser by phone: +31 (0)15-2787088 or by e-mail: firstname.lastname@example.org.
To apply, please submit the following materials by June 15, 2013 using the 'Apply' form above.
- Cover letter explaining your specific interests and qualifications
- Full Curriculum Vitae
- Your MSc thesis (or draft if you are defending in the near future)
- Copies of diplomas and other relevant certificates
- A complete list of attended courses and corresponding grades
- Proof of language skills (if applicable)
- Names and contact details of two references
To meet the early application deadline please apply before June 15. Submissions received after June 15 will be also considered until the position has been filled.
The Department of Software and Computer Technology
The Department of Software and Computer Technology (SCT) of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) of TU Delft comprises the research groups working on core computer science topics. The department is responsible for a large part of the curriculum of the BSc and MSc programmes in Computer Science. The department’s research mission is to perform excellent research at an internationally recognised level in the design, construction and analysis of complex, concurrent and co-operative computer and information systems. Inspiration for the research topics is derived largely from technical ICT problems in industry and society. The department currently consists of the following groups: Parallel and Distributed Systems, Software Engineering, Embedded Software, Algorithms, Web Information Systems, and Computer Engineering.