<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body>
    <p>-------- Forwarded Message --------</p>
    <div class="moz-forward-container">
      <table class="moz-email-headers-table" cellspacing="0" cellpadding="0" border="0">
        <tbody>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">Subject:
            </th>
            <td>[DMANET] One postdoc position at Montpellier University</td>
          </tr>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">Date: </th>
            <td>Tue, 29 Nov 2022 14:03:56 +0100</td>
          </tr>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">From: </th>
            <td>Matthieu Rosenfeld <a class="moz-txt-link-rfc2396E" href="mailto:matthieu.rosenfeld@gmail.com">&lt;matthieu.rosenfeld@gmail.com&gt;</a></td>
          </tr>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">To: </th>
            <td><a class="moz-txt-link-abbreviated" href="mailto:DMANET@zpr.uni-koeln.de">DMANET@zpr.uni-koeln.de</a></td>
          </tr>
        </tbody>
      </table>
      <br>
      <br>
      Dear colleagues,<br>
      in connection with my research project APACE, I am seeking a
      candidate for<br>
      a Postdoctoral position funded for 18 months at LIRMM
      (Montpellier, France).<br>
      <br>
      The APACE project aims at using the links between MSO logic and<br>
      tree-automata over decomposable graph classes to build an
      automatic theorem<br>
      prover. Instead of using the tree-automaton corresponding to an
      MSO formula<br>
      for “efficient” model checking (ie, verifying if a given graph has
      the<br>
      desired property), we will analyze the tree-automaton to deduce
      properties<br>
      of the whole graph class. The first objective is to prove
      algorithmic<br>
      meta-theorems relying on this idea. These algorithms will be
      implemented to<br>
      form the APACE automatic prover. The final objective is to use the<br>
      automatic-prover to obtain new collections of results about
      different<br>
      decomposable graph classes.<br>
      <br>
      The hired candidate is expected to contribute both to the
      theoretical<br>
      aspect of this project and to the implementation (in C++). The
      applicants<br>
      are expected to have a background in theoretical computer science
      and to<br>
      have some programming skills. More precisely, the principal
      expected skills<br>
      for this project are :<br>
      * programming skills (ideally in C++) and algorithmic,<br>
      * computer algebra,<br>
      * graph theory or combinatorics,<br>
      * tree-automata, MSO logic and algorithmic-meta theorems.<br>
      The candidates are not expected to be experts in all of these
      subjects.<br>
      <br>
      The duration of the position is for 18 months, starting between
      February<br>
      and June 2023. The postdoc fellow will be a member of LIRMM. The
      project<br>
      comes with a funding that allows the postdoctoral fellow to travel
      to<br>
      conferences and cover other expenses.<br>
      <br>
      Applications are to be submitted by email to<br>
      <a class="moz-txt-link-abbreviated" href="mailto:matthieu.rosenfeld@umontpellier.fr">matthieu.rosenfeld@umontpellier.fr</a> before December and should
      consist of :<br>
      * a curriculum vitae with a list of publications,<br>
      * a short motivation letter (a few paragraphs inside the email
      suffice).<br>
      <br>
      Informal inquiries are welcomed and should be addressed to<br>
      <a class="moz-txt-link-abbreviated" href="mailto:matthieu.rosenfeld@umontpellier.fr">matthieu.rosenfeld@umontpellier.fr</a>.<br>
      Best Regards,<br>
      Matthieu Rosenfeld<br>
      <br>
    </div>
  </body>
</html>