Grant: Discovery Grants Program - Individual

The presence of defects in software systems of various kinds has important consequences for productivity. At the same time, the thread connecting the inputs of a process to its outputs becomes both longer and thinner. In many cases, retracing the data that contributed to the computation of some result after the fact is, by all practical means, impossible. What is more, without that crucial information, understanding why a process has produced a given result (or failed to produce the expected output) is even harder. In this light, it becomes of paramount importance to properly specify the expected behavior of a system, as well as to develop efficient techniques to test and verify the said system against what is stipulated by its specification. The proposed research program aims at developing formal tools and techniques to help developers identify and fix bugs in various kinds of software systems, with special focus to techniques that make use of a formal specification. In particular, it identifies three broad themes that have been the subject of scant study, and for which a principled approach is required blending theoretical advances and development of practical applications. The first theme is centered around the testing and verification of so-called "stream programs", which can be viewed conceptually as following a design formed of "workflows" or "pipelines" where streams pass through a network of computation stages in order to produce the desired result. The bulk of existing testing literature, which has focused on imperative programming, cannot be directly applied to stream calculations. This first theme stems from the need for a principled approach to stream processing testing; it aims at revisiting and updating elementary software engineering notions such as those of coverage metrics, test oracles or program mutants, to suit the specific paradigm of event stream pipeline. The second theme is framed in the context of what is called runtime verification, where a sequence of events produced by the execution of a system is compared against a formal specification of its expected behavior. Research on this theme aims at expanding the expressiveness of the technique, by considering the problem of runtime verification on sequences expressed as event knowledge graphs (EKGs), as well as introducing specifications that produce a more detailed verdict quantifying the violation of a specification. Finally, the third theme is focused on the explainability of results produced by a testing or verification procedure. In a broad sense, explainability can be seen as a way of linking the outputs of a process to its inputs; this notion is closely related to the concepts of lineage or provenance. It aims at defining the formal foundations of fine-grained explainability, where one should be able to point at a specific part of the output, and be able to derive the corresponding parts of the input that explain the presence of this output.