Open PhD Position in Testing and Verification for Stream-Based Processing

The Formal Computer Science Laboratory (LIF) at Université du Québec à Chicoutimi (https://www.uqac.ca) 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.

• Application deadline: March 31st, 2022
• Starting date: August 31st, 2022

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.

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 25000 CAD per year for three years. Tuition at UQAC is exceptionally low by North American standards: foreign PhD students are expected to pay between 1000 and 2000 CAD per semester.

Application Procedure

Prospective applicants are asked to send by e-mail to Pr. Sylvain Hallé (https://leduotang.ca/sylvain) the following documents, in a message mentioning PhD position **LIF22-D1**:

1. A statement of interest, including the names of 2 external references
2. A CV with a complete list of academic publications
3. Copies of at most 3 selected academic publications
4. Transcripts of bachelor’s and master’s degree
5. Master Thesis, if available

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