Home › Open positions › Open PhD Position in Testing and Verification for Stream-Based Processing (LIF24-D1)

Open PhD Position in Testing and Verification for Stream-Based Processing (LIF24-D1)

Posted on by by Posted in Open positions

The Formal Computer Science Laboratory (LIF) at Université du Québec à Chicoutimi is seeking an outstanding PhD candidate to fill a 3-year funded position on the application of testing and verification for event stream processing and blockchains.

  • Starting date: September 1st, 2024

Project Description

An “event stream” can be defined as a sequence of arbitrary data elements generated by some entity or system. Examples of streams include blockchains made of a dynamically generated sequence of blocks, log files whose lines are produced by the execution of a piece of software, or raw data values emitted by periodical sensor readings. The processing of an input event stream typically results in another output event stream, and the operation can be daisy-chained to perform complex calculations over various event sources. We call “stream program” any calculation that operates on an event stream to produce a desired result: this includes queries expressed in event stream processing languages, code snippets using event stream processing APIs, or smart contracts operating on blockchain elements.

The testing and verification of classical programs has been the subject of thorough study for decades. In contrast, stream programs represent a new paradigm, where concepts and techniques developed for imperative programming cannot be directly transferred. The goal of this doctoral work is to develop the theory, techniques and tools for the testing and formal verification of programs operating on streams, and in particular on stream processing pipelines defined in APIs such as the BeepBeep event stream processing engine (https://liflab.github.io/beepbeep-3). The project involves all at once the development of theoretical concepts related to the testing and verification of stream programs (in particular the notion of coverage), the development of test generation techniques specific to stream programs, the implementation of these techniques into prototypes, and their thorough empirical evaluation. Promising early results on the model checking of such pipelines have recently been published [1] and could be used as a starting point.

Domaine(s) de recherche

  • Testing and verification
  • Formal methods
  • Event stream processing

Environment

Université du Québec à Chicoutimi (UQAC) is part of the largest university network in Canada. It is located in the French speaking Saguenay–Lac-Saint-Jean area, reputed for the beauty of its fjord and the majesty of its natural surroundings. UQAC welcomes 6,500 students every year, more than 1,000 of which coming from 50 different countries. The research program in Computer Science is particularly dynamic; it is the host of two Canada Research Chairs, currently includes around 20 professors and associate professors, 30 PhD and post-doctoral fellows, and more than 100 master’s students.

The doctoral work will be conducted at the Formal Computer Science Lab (https://liflab.ca), under the supervision of Pr. Sylvain Hallé, Canada Research Chair on Software Testing, Specification and Verification. LIF specializes in the application of formal methods to the testing and verification of various software systems. Past projects by faculty members of LIF have been realized in collaboration with numerous companies, including Ericsson, Industrial Alliance, Ubisoft LaForge, Devicom, and Eckinox Média.

Research at LIF is internationally recognized, and contributes to the development of concrete, high-quality software tools grounded in solid mathematical foundations. Notable long-running projects developed at LIF include the BeepBeep 3 event stream processing engine [2], the Artichoke blockchain monitoring system [3], and the Petit Poucet data lineage library [4]. All of these initiatives have been given awards and published in top-tier international conferences over the past decade.

Required Qualifications

A very good Diploma or Master university degree in computer science, informatics, business informatics, mathematics, or a related discipline is expected. We further seek the following qualifications:

  • Very good formal knowledge: formal computer science, automata theory, software specification and testing. A background in mathematics is considered a plus.
  • Good programming skills; knowledge of Java is considered a plus.
  • Knowledge in blockchain technology or cryptography is a plus.
  • Very good scientific communication and writing skills.
  • Very good knowledge in English communication and writing.
  • In-depth interest in scientific problems and the motivation for independent and goal-oriented research.

Funding

Funding of this position is ensured by grants from the Canada Research Chair on Software Specification, Testing and Verification and the Natural Science and Engineering Research Council of Canada. The candidate will receive a scholarship of a net amount of 27,000 CAD per year for three years.

Application Procedure

Prospective applicants are asked to fill the form at https://zfrmz.com/BGLMrz4QFYzkIOZxVtpD?zf_lang=en, make sure to specify project LIF24-D1, and provide the following documents:

  1. Letter of motivation
  2. Curriculum vitae, including a) list of publications if any; b) names and contact information of at least two references
  3. Transcripts of undergraduate and graduate studies
  4. A copy of the Master’s thesis, if it has been submitted

Université du Québec à Chicoutimi is committed to equity, diversity and inclusion at all steps of its students’ curriculum; candidates from under-represented groups are especially encouraged to apply. Applications will be evaluated by a panel of three UQAC faculty members by focusing on the criteria mentioned above. Shortlisted applications will be called for an online interview to further assess their technical and communication skills.

References

  1. A. Bédard, S. Hallé. (2021). Model Checking of Stream Processing Pipelines. In Proc. TIME, 5:1-5:17. DOI 10.4230/LIPIcs.TIME.2021.5
  2. S. Hallé. (2018). Event Stream Processing with BeepBeep 3: Log Crunching and Analysis Made Easy. Presses de l’Université du Québec, ISBN 978-2-7605-5101-5
  3. S. Hallé, R. Khoury, A. El-Hokayem, Y. Falcone. (2016). Decentralized Enforcement of Artifact Lifecycles. In Proc. EDOC, 1-10. DOI 10.1109/EDOC.2016.7579380
  4. S. Hallé, H. Tremblay. (2021). Foundations of Fine-Grained Explainability. In Proc. CAV, Springer LNCS 12760, 500-523. DOI 10.1007/978-3-030-81688-9_24

Candidats au doctorat recherchés: Tests et vérification pour l’event stream processing (LIF24-D1)

Posted on by by Posted in Non classifié(e), Postes ouverts

Le Laboratoire d’informatique formelle à L’Université du Québec à Chicoutimi recherche d’excellents candidats au doctorat pour un projet de doctorat financé de 3 ans sur l’application du test et de la vérification pour le traitement de flux d’événements et les blockchains.

  • Date d’entrée en fonction: 1er septembre 2024

Description du sujet

Un “flux d’événements” peut être défini comme une séquence d’éléments de données arbitraires générés par une entité ou un système. Comme exemples de flux, on peut mentionner des blockchains constituées d’une séquence de blocs générée dynamiquement, des fichiers journaux (logs) dont les lignes sont produites par l’exécution d’un logiciel, ou encore des valeurs brutes émises par des lectures périodiques de capteurs. Le traitement d’un flux d’événements d’entrée se traduit généralement par un autre flux d’événements de sortie, et l’opération peut être connectée en série pour effectuer des calculs complexes sur diverses sources d’événements. Nous appelons “programme de flux” (stream program) tout calcul qui opère sur un flux d’événements pour produire un résultat souhaité: cela inclut les requêtes exprimées dans des langages de traitement de flux d’événements, des extraits de code utilisant des API de traitement de flux d’événements ou des smart contracts opérant sur des éléments d’une blockchain.

Le test et la vérification des programmes classiques font l’objet d’études approfondies depuis des décennies. En revanche, les programmes de flux représentent un nouveau paradigme, où les concepts et les techniques développés pour la programmation impérative ne peuvent pas être directement transférés. L’objectif de ce travail doctoral est de développer la théorie, les techniques et les outils pour le test et la vérification formelle de programmes fonctionnant sur des flux, et en particulier sur des pipelines de traitement de flux définis dans des API telles que le moteur de traitement d’événements BeepBeep (https:// liflab.github.io/beepbeep-3).

Le projet implique à la fois le développement de concepts théoriques liés au test et à la vérification des programmes de flux (en particulier la notion de couverture), le développement de techniques de génération de tests spécifiques aux programmes de flux, la mise en œuvre de ces techniques dans des prototypes, et leur évaluation empirique approfondie. Des premiers résultats prometteurs sur le model checking de tels pipelines ont récemment été publiés [1] et pourraient être utilisés comme point de départ.

Domaine(s) de recherche

  • Test et vérification
  • Méthodes formelles
  • Traitement de flux d’événements (stream processing)

Présentation établissement et labo d’accueil

L’Université du Québec à Chicoutimi (UQAC) fait partie du plus grand réseau universitaire au Canada. Elle est située dans la région francophone du Saguenay–Lac-Saint-Jean, réputée pour la beauté de son fjord et la majesté de sa nature environnante. L’UQAC accueille chaque année 6 500 étudiants, dont plus de 1 000 provenant de 50 pays différents. Le programme de recherche en informatique est particulièrement dynamique; il est l’hôte de deux chaires de recherche du Canada, comprend actuellement une vingtaine de professeurs, 30 doctorants et boursiers postdoctoraux et plus de 100 étudiants à la maîtrise.

Le travail de doctorat se déroulera au Laboratoire d’informatique formelle, sous la supervision du Pr. Sylvain Hallé, titulaire de la Chaire de recherche du Canada sur les tests, la spécifications et la vérification de systèmes informatiques. Le LIF est spécialisé dans l’application de méthodes formelles au test et à la vérification de divers systèmes logiciels. Les projets antérieurs des membres du corps professoral du LIF ont été réalisés en collaboration avec de nombreuses entreprises, dont Ericsson, Industrielle Alliance, Ubisoft LaForge, Devicom et Eckinox Média.

La recherche au LIF est reconnue internationalement et contribue au développement d’outils logiciels concrets et de haute qualité fondés sur des bases mathématiques solides. Les projets notables de longue date développés au LIF incluent le moteur de traitement de flux d’événements BeepBeep 3 [2], le système de surveillance de la blockchain Artichoke [3] et la bibliothèque de lignage de données Petit Poucet [4]. Toutes ces initiatives ont été récompensées et publiées dans des conférences internationales de premier plan au cours de la dernière décennie.

Profil de la candidature

Un très bon diplôme de maîtrise universitaire en informatique, informatique de gestion, mathématiques ou dans une discipline connexe est attendu. Nous recherchons en outre les qualifications suivantes:

  • Très bonnes connaissances formelles: informatique formelle, théorie des automates, spécification et test de logiciels. Une formation en mathématiques est considérée comme un plus.
  • Bonnes compétences en programmation; la connaissance de Java est considérée comme un plus
  • Des connaissances en technologie blockchain seront considérées.
  • Très bonnes aptitudes à la communication scientifique et à la rédaction.
  • Très bonne connaissance de la communication et de l’écriture en anglais.
  • Intérêt marqué pour les problèmes scientifiques et motivation à mener une recherche indépendante et ciblée.

L’Université du Québec à Chicoutimi s’engage pour l’équité, la diversité et l’inclusion à toutes les étapes du cursus de ses étudiants; les personnes des groupes sous-représentés sont particulièrement encouragées à postuler. Les candidatures seront évaluées par un panel de trois membres du corps professoral de l’UQAC en se concentrant sur les critères mentionnés ci-dessus. Les personnes sélectionnées dans un premier temps seront convoquées pour un entretien en ligne afin d’évaluer davantage leurs compétences techniques et de communication.

Eléments à fournir pour la candidature

Les personnes souhaitant sont invités à remplir le formulaire en ligne à l’adresse https://zfrmz.com/BGLMrz4QFYzkIOZxVtpD en prenant soin de choisir le concours LIF24-D1 et en fournissant les documents suivants:

  • Lettre de motivation
  • Curriculum vitae, incluant a) la liste des publications le cas échéant; b) les noms et coordonnées d’au moins deux références
  • Relevé de notes du baccalauréat (licence) et de la maîtrise (master)
  • Une copie du mémoire de maîtrise, si celui-ci est déposé

Références

  1. A. Bédard, S. Hallé. (2021). Model Checking of Stream Processing Pipelines. In Proc. TIME, 5:1-5:17. DOI 10.4230/LIPIcs.TIME.2021.5
  2. S. Hallé. (2018). Event Stream Processing with BeepBeep 3: Log Crunching and Analysis Made Easy. Presses de l’Université du Québec, ISBN 978-2-7605-5101-5
  3. S. Hallé, R. Khoury, A. El-Hokayem, Y. Falcone. (2016). Decentralized Enforcement of Artifact Lifecycles. In Proc. EDOC, 1-10. DOI 10.1109/EDOC.2016.7579380
  4. S. Hallé, H. Tremblay. (2021). Foundations of Fine-Grained Explainability. In Proc. CAV, Springer LNCS 12760, 500-523. DOI 10.1007/978-3-030-81688-9_24

Top

Discover more from LIF

Subscribe now to keep reading and get access to the full archive.

Continue reading