PostDoc on Computer Aided Verification of Automata (TUM, Munich, Germany)

We are seeking a PhD student or post-doc to work on the CAVA project at TUM. The aim of the CAVA project is to formalise and verify important algorithmic parts of automata theory and model checking in the theorem prover Isabelle. A recent result is a verified Spin-like model checker with performance comparable to Spin.

Applicants must have an MSc or PhD in Computer Science or a closely related field. A keen interest in theoretical computer science and verification is essential. The position is for two years with potential renewal contingent on funding. Starting date is asap but negotiable.

Applications should include:

  • a curriculum vitae
  • a brief statement of the particular contribution you would like to make to the project
  • the names and contact details of two referees.

Enquiries and applications should be sent to Tobias Nipkow.

Posted in PostDoc | Comments Off

PostDoc on Realizability for Classical Logic, Concurrency, References and Rewriting (PPS Laboratory, Paris-Diderot University, France)

A postdoctoral position is available at our PPS laboratory in Paris for the next academic year.

The position is supported by the ANR project RECRE “Realizability for classical logic, concurrency, references and rewriting” which brings together researchers working in four different sites: the LIP at ENS Lyon, PPS at University Paris Diderot, IML in Marseille and LAMA in Chambery.

The scientific goal of the project consists in investigating syntactic as well as semantic models of computations based on realizability, and to understand their connection to imperative and concurrent programming languages, as well as to advanced type systems (typically dependent).

More information on the ANR RECRE website.

Requirements are a PhD degree in Computer Science or Mathematics and a strong background in some of the following topics:

  • realizability (classical realizability, forcing)
  • proof theory (dependent types, classical logic, linear logic)
  • semantics of effects (monadic effects, algebraic theories)
  • categorical semantics (realizability topos, homotopy type theory)

The position is starting fall 2013 for one year. The salary is standard french postdoc, with benefits such as health insurance.

Applications must include a research statement, a CV and the names and contacts of references. All material should be sent by email to:

  • curien(at)
  • herbelin(at)
  • mellies(at)

Important dates:

  • Intention of application (short email): as soon as possible
  • Deadline for application: August 1st, 2013
  • Suggested starting dates: Sep.-Dec. 2013
Posted in PostDoc | Comments Off

PostDoc on Homotopy Type Theory (Carnegie Mellon University, Pittsburgh, PA, United States)

The Department of Computer Science of Carnegie Mellon University seeks applicants to fill the position of a 9 months Post Doctoral Fellow in the Computer Science Department. Under the direction of the principal investigator, the incumbent will conduct and lead research in the field of theory of computation, particularly intuitionistic type theory and its application to homotopy theory. Specific duties will include conduct of fundamental research into the computational semantics of homotopy type theory with applications to programming languages and automated reasoning. In addition, the successful candidate is expected to coordinate research with other members of the CMU community, as well as minimally supervise junior members of the group. The appointment is for one year with the possibility of renewal, pending available funding and satisfactory performance.

Minimum Qualifications

  • Education: Ph.D. in theoretical computer science or mathematics
  • Experience: Strong background in: proof theory, category theory, categorial logic, type theory or related areas. Exeprience in: functional programming, semantics of programming languages, mechanized reasoning.
  • Skills: The successful candidate must have proven supervisory and leadership skills, and the ability to coordinate report findings and take lead in composing research proposals, specifically in response to broad agency announcements. Demonstrated ability to manage multiple priorities; and communicate effectively in an interdisciplinary environment.
  • Physical Mobility: Ability to travel to various campus locations as needed. Able to lift and bend and move equipment. May be required to work at computer for extended periods of time.
  • Mental: Must be able to communicate effectively in verbal, written and presentation forms. Ability to work under pressure, pay attention to detail, meet inflexible deadlines, and deal with difficult people while maintaining composure.
  • Other: Normal office or laboratory environment

To apply, go to this page and use job number 100196. For more information about this position, contact Prof. Robert Harper.

Posted in PostDoc | Comments Off

PostDoc in Combined Static and Dynamic Program Analyses (VirginiaTech, Blacksburg, VA, United States)

PROLANGS@VT is interested in the use of program analysis to ensure software quality of real-world applications. Current focus is on the use of combined static and dynamic program analyses for object-oriented scripting languages such as JavaScript. Algorithm design and empirical validation are key characteristics of our work. Emphasis on approaches effective and practical for real applications in security, debugging, and software tools. Postdoc’s primary responsibility to strengthen research group and help with research supervision of graduate/undergrad student researchers.

Applicants must have a PhD in computer science or a closely related field and must be self-motivated and willing to take the initiative in research. Some background in experiment design, program analysis, experience with compiler-based frameworks (e.g., SOOT, WALA), and/or use of Eclipse and CVS-like repositories is desirable.

The term of the postdoc is one year with a possible extension. Starting date: as soon as possible, but negotiable. If interested, please send a CV, research statement, and the names of three references with their email addresses to Dr. Barbara G. Ryder (ryder(at)

Posted in PostDoc | Comments Off

PostDoc on Weak-Memory Concurrency and Compilation (ENS Paris, France)

The Parkas team (ENS — INRIA, Paris, France) is seeking applicants for a post-doctoral position to join our group working on the broad area of concurrency and compilation.

Recent work focussed on the relaxed-memory concurrency that real systems exhibit, including work on the memory models of multiprocessors (x86, Power, ARM), verified compilation of concurrent programming languages to multiprocessors, the semantic theory of relaxed-memory concurrency, the development of tool support for semantics, and compiler testing.

Applicants must have a PhD in Computer Science or a closely related field. The term of the postdoc position is one year with an option to renew for another year. Starting date is negotiable (tentatively October 2013). A keen interest in programming languages, concurrency, semantics, and compilation is essential.

The position is funded by the ANR WMC project led by Francesco Zappa Nardelli.

Applications should include:

  • a curriculum vitae
  • a brief statement of the particular contribution you would like to make to the project
  • the names and contact details (postal and e-mail addresses) of two referees.

Applications and enquiries should be sent before July 15th to francesco.zappa_nardelli (@)

Posted in PostDoc | Comments Off

PhD on Synthesis of Maximal Invariants for Controlled Switched Systems (CEA/ENS Cachan, France)

PhD position at CEA LIST (Atomic Energy Commission, Saclay, France) and LSV (CNRS & ENS Cachan, France)

We have one opening for a project called “Synthesis of Maximal Invariants for Controlled Switched Systems”.

Switched systems are embedded devices widespread in industrial applications such as power electronics and automotive control. They consist of continuous-time dynamical subsystems and a rule that controls the switching between them. Under a suitable control rule, the system can improve its steady-state performance and meet essential properties such as safety and stability in desirable operating zones (see e.g. Laurent Fribourg, Romain Soulat. “Controlled Recurrent Subspaces for Sampled Switched Linear Systems“, Research Report LSV-12-24).

The project focuses on the automatic determination of a maximal stability zone of a (differential) system, and its associated (discrete) controller. The techniques involved are:

  • set-based numerical methods (interval methods, affine forms, Taylor models…) and inner-approximations
  • non-linear control
  • some validation methods in the large (abstract interpretation, model-checking etc.)

This project is located both at CEA LIST, in Saclay, 25km south of Paris and in ENS Cachan, 5 km south of Paris.

Interested candidates are invited to contact the principal investigators Eric Goubault/Sylvie Putot eric.goubault(at) and Laurent Fribourg laurent.fribourg(at)

Posted in PhD | Comments Off

PostDoc on Verification of Highly Configurable Software Systems (IT University Copenhague, Denmark)

Two projects, VARIES and VARIETE, seek excellent post-doc candidates to work on analysis methods for code and models found in highly configurable software systems (software product lines).

Application deadline: 4th August, 2013 at 23.59 CET.
Continue reading

Posted in PostDoc | Comments Off

PhD in Computer Science (Leicester University, United Kingdom)

The University of Leicester has 3 positions GTA positions available in computer science. Graduate Teaching Assistantships funds a PhD through limited part-time teaching work with the University. The deadline for the application is 29 July 2013.

The topics of particular interest are the following:

  • Software Modularity Constructs for Relating Requirements to Implementation
  • p-Automata and Related Games
  • Synthesis of Controllers from Temporal Specifications
  • Dynamic Adapation of Workflows
  • Biology Inspired Modelling of Distributed Computing
  • Reversible Debugging and Concurrency

More information about these topics here.

Full offer here.

Posted in PhD | Comments Off

PostDoc on Graph Theory (Durham University, United Kingdom)

A Research Associate (RA) is sought, with expertise in graph algorithms and complexity, preferably also in parameterized complexity and/or intersection graphs. The successful candidate will work at Durham University under the guidance of Dr. George Mertzios on the EPSRC-funded grant “Algorithmic Aspects of Intersection Graph Models”. The research in this grant will explore the geometric intersection models by which many important families of graphs can be represented, in order to devise efficient algorithms or prove computational hardness (from both the classical and the parameterized point of view) for fundamental optimization and recognition problems. More details on the grant can be found on this page. The successful candidate will be part of the Algorithms and Complexity research group (ACiD) in the School of Engineering and Computing Sciences at Durham University.

This post is available from the 1st of October 2013 and is fixed term for 12 months.

Continue reading

Posted in PostDoc | Comments Off

PostDoc on Concurrency and Compilation (ENS Paris, France)

The Parkas team (ENS – INRIA, Paris, France) is seeking applicants for a post-doctoral position to join a group working on the broad area of concurrency and compilation.

Application deadline: July 15th, 2013.
Continue reading

Posted in PostDoc | Comments Off