Announcement of PhD Funding

We are urgently looking for a PhD candidate for the following proposal that we are in the process of submitting for joint funding by Inria and the French Agency for Defence Innovation (AID). Due to the AID constraints, only candidates holding EU, United Kingdom or Swiss citizenship can apply.

Please do forward this information to potential candidates.

The main objective of this project is to contribute to the implementation of modular robots by developing a formal framework to model, validate and coordinate their dynamic behaviours. The scientific challenges consist in particular in the ability to model the dynamic evolution of this type of complex systems—their adaptation and reconfiguration—by taking into account constraints on resources as well as events occurring in their execution environment.

Host institution: Inria Lille – Nord Europe, team Spirals

Additional information:

Any questions can be addressed to us by e-mail (see below). Detailed description of the project is available at

me/simon/2022/03/modular-robots-phd/

Best regards,

Simon Bliudze <simon.bliudze@inria.fr> Sophie Cerf <sophie.cerf@inria.fr> Olga Kouchnarenko <olga.kouchnarenko@univ-fcomte.fr>

The Department of Computer Science at Aarhus University, Denmark, offers two PhD positions in the area of Algorithmic Verification. The research topics are focused on the automated analysis of concurrent systems, as well as algorithmic aspects of static analyses of sequential/concurrent programs. Applicants are expected to have strong analytical skills in Computer Science and a personal drive for research.

Admission can be on the basis of either a BSc or an MSc degree. Tuition is fully covered, and a generous stipend is provided for the full duration of the PhD.

Interested applicants are encouraged to contact pavlogiannis@cs.au.dk<pavlogiannis@cs.au.dk>, enclosing a CV.

Next deadline: May 1, 2022 Application website: dk/for-applicants/open-calls/february-2022-1/re-advertisement-programming-language-design-analysis-and-verification-1__;!!IBzWLUs!Dq3Uec0Q_haJTyMJrB7LzHBToxXzm15seZ1SV8O7CXSdRdS_zIDyM4qBvG-4SBhJ78vy2L72ZVpj1g$ Information about our PhD program: dk/for-applicants/application-guide/__;!!IBzWLUs!Dq3Uec0Q_haJTyMJrB7LzHBToxXzm15seZ1SV8O7CXSdRdS_zIDyM4qBvG-4SBhJ78vy2L4SOp-xUQ$

Announcement for a PhD position funded by the ANR ReciProg.

Project summary. RECIPROG is an ANR collaborative project starting in the fall 2021-2022 and running till the end of 2025. ReCiProg aims at extending the proofs-as-programs correspondence (aka Curry-Howard correspondence) to recursive programs and circular proofs for logics and type systems using induction and coinduction. The project will contribute both to the necessary theoretical foundations of circular proofs and to the software development allowing to enhance the use of coinductive types and coinductive reasoning in the Coq proof assistant.

Informations - The PhD research shall take place under supervision of Luigi Santocanale (LIS, Aix-Marseille Université) and Pierre Hyvernat (LAMA, Université de Savoie) - The foreseen starting date of the PhD shall be on September 2022 (negotiable). - More informations on the RECIPRIG project can be found at fr/reciprog/

Application process: - There is no strict deadline for applications. A first screening of applications shall take place on Mai 16, 2022, please send your application before that date. - Candidates can send their application to Luigi Santocanale and Pierre Hyvernat (luigi.santocanale@lis-lab.fr, pierre.hyvernat@univ-smb.fr) with a subject containing “[RECIPROG PhD application]”. - The application should contain a CV, transcripts of marks, and contacts of reference persons (or reference letters if available).

Title of thesis: Semantic methods for circular proofs

Description. Formal proofs are usually presented as well founded trees. By allowing cycles in proofs, circular proofs come as a generalization and naturally formalize recursive proofs and programs.

Not all circular proofs are correct. As an instance of the halting problem, separating correct circular proofs from the incorrect ones is not possible. By now, most circular proof systems are based on fragments of linear logic extended with least and greatest fixed points. A first circular proof system [Santocanale, 2002, Fortier and Santocanale, 2013] restricted proofs with a strong syntactical condition guaranteeing that each proof has a well defined categorical semantics. More recent work [Doumane, 2017] considered a more liberal correction criteria, based on parity automata, which ensures a well-behaved cut-elimination procedure.

It is natural to extend the Curry-Howard-Lawvere correspondence to circular proof systems. Indeed, functional languages like Haskell or Caml have inductive types (least fixed points, initial algebras) and allow recursive definitions. Languages like Coq or Agda, based on dependent type theory, also have a notion of coinductive types (greatest fixed points, terminal coalgebras). Validating a recursive proof may differ: Coq uses a simple syntactical criterion while Agda uses a complex algorithm based on the size-change principle that accepts many more definitions.

Extending the Curry-Howard-Lawvere to such languages is difficult because they are very expressive and are not based on linear logic. Ideally, the doctoral student shall achieve this goal. He will start with relating the different approaches: the “categorical” one, that relies on solid algebraic ideas which however need to be extended to consider monoidal up to locally Cartesian closed categories; the “logical” one, based on linear logic, with a rather simple proof theory and many good properties; and the “programming” approach, based on very expressive type theories but where the proof theory of circular proof hasn’t been studied as extensively.

The goal is to extend well-behaved circular proof system to get closer to real programming languages, adequate for formalization. Recognizing that a recursive definition is correct is undecidable in general and Agda’s algorithm is (supposedly) correct but incomplete. Unfortunately there is no proof of correctness for a dependent type system. It is thus important to see if the technology developed for linear systems can be extended to full dependent types, and how.

-- Luigi Santocanale, professeur, LIS/AMU

Ph.D position in Formal Methods available at the Dept. of Informatics, University of Oslo. The topic is "Formal Analysis for Concurrent Programs".

1. Position

 The position will be part of the research
  group on formal methods at the Department
  of Informatics (IFI). The research group
  develops and applies techniques for formal
  modelling and analysis in a range of
  problem domains. As a research fellow in
  this research group, you will be working in
  a friendly, stimulating and international
  research environment with a number of PhD
  and postdoctoral fellows.

2. Qualification requirements, employment details & how to apply

  For detailed information about how to
  apply, formal application requirements and
  expectations, terms of employment and wage
  etc., see the web announcements:

  - no/en/available-jobs/job/222897/phd-research-fellow-in-formal-analysis-of-concurrent-systems__;!!IBzWLUs!FPggx67PTjENQl-UxY3_A1TpO3eJYtOvN9_w60oLr9JWoF1KI3vQ8V1a34G7jZ4BsBd96oLLA4c0Qg$ 

3. Contacts:

  - Martin Steffen             (msteffen@ifi.uio.no)
  - Einar Broch Johnsen        (einarj@ifi.uio.no)

4. More details on the intended area of research

  The planned PhD research aims to develop
  formal semantic-based analysis methods for
  tackling modern concurrency abstraction and
  memory models for multi-threaded
  programming languages and systems. That
  also involves developing and using
  appropriate software analysis and synthesis
  tools to ensure synchronisation-related
  correctness properties, such as
  deadlock-freedom, sequential consistency,
  functional determinacy or absence of
  information leakage. The results from the
  theoretical investigations will be
  encapsulated in programming libraries and
  analysis algorithms that fit into the
  existing eco-systems of the chosen host
  languages.

  Methodologically, the research will target
  mainly light-weight verification methods,
  analysis methods and corresponding tools
  that work automatically, without
  interactive user intervention. In
  particular, type-based analyses and
  synthesis methods to check for
  resource-consumption, conformance with
  interface specification, race freedom, etc.

The ORKAD team at University of Lille, is looking for a full-time PhD student to work on a project mixing parameterized complexity and multiobjective optimization. The PhD will be supervised by Laetitia Jourdan and Julien Baste. If the application is accepted, we offer a fully funded position for a period of 3 years. This work should lead to a PhD degree. The detail of the PhD is attached to the email.

Applicants for the PhD position should hold a master's degree in computer science or mathematics. In order to apply, the student should send a fully detailed CV, an academic record (Master degree or equivalent), a cover letter, and at least one recommendation letter. The application should be sent before April 23th 2022 to phd-application-orkad-2022@univ-lille.fr. If you have any question regarding the offer, feel free to send us an email to phd-application-orkad-2022@univ-lille.fr.

Regards,

-- Julien Baste julien.baste@univ-lille.fr

baste/

Une bourse de thèse est proposée pour la rentrée 2022 à l'ICB dans le cadre du projet Région TACTICQ (Techniques Avancées de Calcul pour la Théorie de l'Information et du Contrôle Quantique). Il s'agit d'une thèse sur le calcul quantique dont l'intitulé est "Measuring Quantum entanglement and quantum contextuality with a Noisy Intermediate Quantum Computer". L'objectif principal de la thèse est de chercher à évaluer sur des machines quantiques des outils mathématiques (invariants algébriques, inégalités) utilisés pour distinguer les classes d'intrications quantiques ou encore mesurer la contextualité de configurations d'opérateurs de Pauli.

Les candidatures sont ouvertes aux candidats ayant un master en mathématiques, physique ou informatique ou encore aux diplômés des écoles d'ingénieur. N'hésitez pas à transmettre aux étudiants qui pourraient être intéressés. Ci-dessous le lien avec les informations pour candidater,

pdf

PhD Scholarship Heriot-Watt University, Scotland

The Lab for AI and Verification (laiv.uk), Heriot-Watt, Edinburgh, Scotland is looking to fill in one PhD post. We are looking for a candidate with solid knowledge of Theorem Proving and/or Functional/Logic programming, and enthusiasm to apply this knowledge in the domain of Artificial Intelligence.

The post is for 4 years, starting in September 2022. It covers full stipend and PhD fees, and is sponsored by the UKRI (ukri.org) and Schlumberger Cambridge (slb.com). The company will provide additional training and support during the PhD studies.

Please direct all queries to Matthew Daggitt (m.daggitt@hw.ac.uk) and Ekaterina Komendantskaya (ek19@hw.ac.uk) by the 3rd April 2022.

Nous recherchons un doctorant pour une offre de thèse à Inria Lille, co-encadrée par Pierre Bourhis et moi-même, sur l'explication et les circuits pour l'évaluation de requêtes et le raisonnement logique.

L’objectif de la thèse est d'étudier de façon fine les problèmes liés à l'explication des raisonnements logiques faits dans plusieurs cadres : l'explication d'interrogation de bases de données par des requêtes, l'inférence de données par des règles logiques et l'exécution de programmes définis par des règles logiques comme les data-centric workflows.

Le lien de candidature et plus d'informations sont disponibles sur le portail Inria fr/public/classic/fr/offres/2022-04484 et la date limite pour candidater est le 8 avril.

Université Grenoble Alpes and Decyphir SAS welcome applications for a fully-funded PhD position in Machine Learning Enabled Cyber-Physical Systems, starting in 2022.

PhD Title: Coverage Measures for Machine Learning Enabled Cyber-Physical Systems

html

Cyber Physical Systems (CPS) are systems mixing software and hardware (cyber) components in interaction with their (physical) environment. Typical examples includ autonomous cars, robots, medical devices. Mathematically, they are modelled with so-called hybrid systems, which are dynamical systems with multiple modes, which can be continuous or discrete in nature. Since the modelisation includes the physical/biological environment, the models can be of arbitrary complexity, from trivial (not all models need be complex to be useful) to untractable for nowadays computational resources due to the infiniteness of input and state spaces of these systems. Hence new methods and tools are always needed to manage and handle the type of heterogeneous computations and data generated by the analysis and design of hybrid systems.

In this thesis, we want to tackle this issue from the angle of coverage measures. Given a CPS problem and some data and/or models (e.g., a hybrid system) associated to it, the question is: what is the mathematical domain that can represent all possible data that can be observed, and can we measure how well the given data represent this domain? This question is of primordial theoretical and practical interest in many contexts. One popular contemporaneous instance is that of machine learning (ML). It is well-known that ML-based algorithms, which are more and more used for CPS design, are only as good as the data used to train them. However it is much less well understood how to formally define the “goodness” of the data at our disposal. Hence there is a need for meaningful measures that can be computed and used not only to quantify the quality of a set, but also to fix it by, e.g., shrinking or augmenting it to better represent a domain to learn.

The questions of coverage, sampling, data augmentation, ML, CPS, etc are not new and topics that have attracted a lot of interest recently. The originality of this thesis will be to tackle these problems from the perspective of hybrid systems and formal methods, which are two research directions in which Verimag and Decyphir are specialized into and internationally recognized for. The intrinsic hybrid nature of data and systems considered in machine learning for CPS is often overlooked and we believed there is a need to study it in a more systematic and explicit way. Formal methods makes it possible to derive more rigorous guarantees and the hope is also that through the use of specification languages such as, e.g., Signal Temporal Logics (STL), they can help in the development of “explainable” measures, i.e., measures that are directly related to precisely formulated requirements as opposed to some hard to interpret mean squared error quantity as is the most frequent practice. Application

The thesis is fully funded for three years by a grant from region Auvergne-Rhône-Alpes starting in 2022. We are looking for candidates with a Master degree in computer science or control engineering interested in CPS, artificial intelligence and machine learning. The thesis is expected to feature a strong experimental and development component but opportunities to developping theoretical contributions will also be likely. As a consequence, candidates with both theoretical and practical inclinations are welcome to apply.

Send applications (resume and motivation letter) to thao dot dang at univ-grenoble-alpes dot fr and alex at decyphir dot com

The Department of Mathematics of Vrije Universiteit Amsterdam welcomes applications for a fully-funded, 4-year PhD position in Number Theory and Formalization.

The preferred starting date is in the period 1 May - 1 September 2022.

The candidate will conduct research on Sander Dahmen's NWO-funded project "Formalizing Diophantine algorithms". This amounts to both developing and formalizing (with a proof assistant such as Lean or Coq) number theory necessary for solving Diophantine problems. The focus will be on effective/algorithmic number theory, but more "pure" results will (necessarily) also play an important role. We note that in this project most of the time will likely be spent on actual formalization work and that the proof assistant to be used will probably be Lean (but that is open for discussion). The position also contains a small teaching component.

The research will be embedded in the Algebra and Number Theory group of the Mathematics Department and in particular connects to the CAN-endowed chair "Automated verification of mathematical proof" held by Assia Mahboubi. Within the Faculty of Science there will also be close collaboration with (Theoretical) Computer Science, especially the group of Jasmin Blanchette.

Applications from all groups currently under-represented in academic posts are particularly encouraged. We are working to improve the present gender balance within the department, and particularly welcome applications from women.

More details at

nl/ad/phd-position-number-theory-and-formalization/70lg5t

A funded PhD student position is proposed in LAMSADE, University Paris Dauphine on Communities in Networks: Detection of dense subgraphs and partitions.

The ideal candidate has a keen interest and strong background in combinatorial optimization, graph theory, exact complexity. Notions on parameterized complexity and approximation algorithms are a plus. He/she must have a Master degree or equivalent in these areas. He/she should have excellent academic qualifications.

The position is fully funded for 3 years. There is no obligation to teach, but it will be possible (with additional payment). Funding for attending international conferences, summer schools, and visiting other research centers will also be provided. Starting date is expected in September-October 2022.

Any interested candidate is invited to email his/her application (including CV, letter of motivation, academic record during the last two years and possibly the name and email of reference persons) to cristina.bazgan@dauphine.fr by April 20th, 2022.

PhD opportunity - GeoDeep4Mesh: Geometric Deep Learning on the Mesh - AI_PhD@Lille, France

We are looking for PhD student candidates on the following subject: Geometric Deep Learning on the Mesh (GeoDeep4Mesh).

Abstract of the PhD

While deep learning methods have been studied for quite a long time on regular domains like for images, learning solutions capable of working on non-Euclidean data like graphs, meshes or point clouds have been defined more recently. This area of research is attracting more and more interest for the potential applications in many disparate domains, going from modeling of social networks, molecules matching and design, to surface classification and recognition. This has originated a new area of investigation broadly known as Geometric Deep Learning. In this thesis proposal, we aim at investigating new solutions for learning on 3D meshes. On the one hand, our idea is to attack the problem by proposing equivariant networks capable of accounting for 3D transformations as well as embedding new metrics in the loss that are computed on the surface. On the other hand, we will propose generative models for meshes and point clouds that also account for the temporal dimension.

Click on for more details

com/file/d/1zwHWPB8jFp6lQGOCm0SGuAYwHnzWyLnG/view?usp=sharing

Key words: 3D mesh, geometry, deep learning, face, human body.

Required skills

• The applicant should conduct Master or engineering studies in relevant fields (artificial intelligence, data science, mathematics).
• Strong algorithm and programming skills (PyTorch/Keras/Python/etc.).
• Familiarity with Riemannian/Differential geometry
• Familiarity with deep learning in computer vision

The applicant should send an email to Prof. mohamed.daoudi@imt-nord-europe.fr subject [GeometricDeep] including at least:

1. A detailed CV 2. A motivation letter 3. Reference letters 4. University transcripts 5. Application deadline: April 1st

The PhD thesis will be funded in the framework of the AI_PhD@Lille program. php/en/phd-in-artificial-intelligence/

International collaborations

In this project, we will collaborate with the Media Integration and Communication Center (MICC), of the University of Florence.

The candidate will be funded for 3 years; he/she is expected to defend his/her thesis and graduate by the end of the contract. The monthly gross salary is around 2000€, including benefits (health insurance, retirement fund).

The position is located in Lille, France. With over 110 000 students, the metropolitan area of Lille is one France's top education student cities. The European Doctoral College Lille Nord-Pas de Calais is headquartered in Lille Metropole and includes 3,000 PhD Doctorate students supported by university research laboratories. Lille has a convenient location in the European high-speed rail network. It lies on the Eurostar line to London (1:20 hour journey). The French TGV network also puts it only 1 hour from Paris, 35 mms from Brussels, and a short trips to other major centers in France such as Paris, Marseille and Lyon.