Research

Until May 2025, I was a postdoctoral researcher at the Software Languages Lab of Vrije Universiteit Brussel (Brussels, Belgium), after obtaining my PhD there in November 2024. My work involved the development of a general incrementalisation technique for static program analyses, based on the dependencies between program parts, applicable to highly-dynamic higher-order languages.

Discover more about my research at the bottom of this page. You can find my research profiles or contact me using the buttons below.

Below you can find an overview of my theses and publications. Click on the titles to read the abstract. When available, links to the presentations and to the slides have been included.

Theses

Van der Plas, J., (2024). Incremental Static Program Analysis through Reified Computational Dependencies. (Doctoral dissertation, Vrije Universiteit Brussel). ISBN: 978-94-6494-861-5.

Over the last few decades, computers have become an indispensable part of modern society. As the programs running on these computers play an essential role in everyday life, for example in banking and communication, it is crucial that they are reliable. To this end, developers have come to rely on static analysis tools to verify a wide range of program properties without actually running the program. Static analyses are typically integrated into modern software development environments and continuous integration systems to safeguard software quality throughout the entire development process.

During the development process, software developers continuously apply small changes to the program. It is therefore not only important for a static analysis to deliver precise feedback, but also to efficiently update its feedback whenever the program is modified. To this end, an incremental static analysis avoids a full recomputation of the analysis result. Instead, upon a change in the program, it reuses and updates the previously computed result, saving valuable analysis time.

It is challenging to develop an incremental analysis that is sufficiently powerful to verify a wide range of program properties and that supports complex language features found in contemporary programming languages. In this work, we present a novel generic approach to construct such analyses by using reified computational dependencies. We show how an analysis that reifies the computational dependencies within the analysed program can be rendered incremental. By relying on these dependencies, our incremental analysis restricts the impact of a change to the affected parts of the analysis result. Moreover, we impose minimal requirements on the analysis itself, allowing a broad applicability of our approach to incrementalisation.

To preserve the precision of the resulting incremental analysis, we introduce three complementary result-invalidation strategies that limit the loss in precision. These strategies are built around the core idea of interleaving invalidation with computation.

Van der Plas, J., (2019). Incremental Thread-Modular Static Analysis for Concurrent Programs with Futures and Atoms. (Master’s thesis, Vrije Universiteit Brussel).

Building concurrent programs is hard as the use of multiple threads introduces nondeterminism in their executions. This nondeterminism leads to bugs that are often subtle to detect and difficult to resolve. Having tool support to detect such program defects may significantly reduce the effort required to resolve concurrency-related bugs.

In recent years, multiple programming paradigms and programming constructs have been developed to facilitate the development of concurrent programs. However, incorrect use of these constructs may cause bugs. Atomic variables, or atoms, are an example of such constructs and can be found in modern programming languages such as Clojure. Atoms provide concurrent but race-free updates to shared state. In this dissertation, we apply the Abstracting Abstract Machines (AAM) technique of Van Horn & Might, a well-known technique to build abstract interpreters, to a concurrent language containing futures and atoms. We formalise this language using a parallel CESK machine which is then systematically abstracted, obtaining the first AAM-based abstract interpreter able to analyse a concurrent language with atoms.

An important aspect of an abstract interpreter is its performance. To be sound, an abstract interpreter for concurrent languages must account for all possible thread interleavings in a concurrent program. Recent work has already introduced thread-modular analysis techniques to reduce the worst-case time complexity of such analyses. Recently, Stiévenart has introduced ModConc, a general approach to the design of thread-modular analyses. The approach results in an analysis that alternates between two phases: an intra-process analysis phase analyses each thread in isolation, while an intra-process analysis phase tracks the behaviour of all threads and invokes intra-process analyses where necessary. In this dissertation, we improve this algorithm by introducing incrementality. We construct the results of the intra-process analysis in an incremental way by allowing results from prior invocations to be reused. This way, we aim to reduce the analysis time needed by the abstract interpreter, making the analysis more scalable to large, real-world programs. Furthermore, we investigate additional optimisations that are possible.

We evaluate our incremental analysis algorithm on a set of benchmark programs and show that it reduces the average analysis time for most of our benchmark programs compared to the original non-incremental algorithm. For several benchmarks, we find significant reductions of the average analysis time, ranging from 40% up to 63%. On multiple occasions, the size of the resulting abstract state graph is reduced as well, leading to fewer spurious paths in the result graph. We find that IncAtom succeeds in reusing large parts of previously calculated results for some benchmarks.

In summary, in this dissertation, we introduce an AAM-based incremental thread-modular analysis and apply this to a concurrent language with futures and atoms. By doing so, we not only extend the application domain of AAM-based analyses but also introduce a new algorithm that improves the performance of thread-modular analyses, thereby improving their scalability and making them applicable to increasingly large programs.

Van der Plas, J., (2017). Ondersteuning voor R5RS-Scheme in het Scala-AM Framework (Bachelor’s thesis, Vrije Universiteit Brussel).

Dit verslag is het eindrapport van de bachelorproef. Het doel van deze bachelorproef is het uitbreiden van SCALA-AM, een framework dat gebruikt wordt voor statische codeanalyse van Scheme-programma’s die aan de R5RS Scheme-standaard voldoen. Op dit moment worden nog niet alle R5RS-taalfeatures door SCALA-AM ondersteund. Dit heeft als gevolg dat Scheme-programma’s die van niet-ondersteunde R5RS-features, zoals quasiquoting, macro’s en sommige taalprimitieven, gebruikmaken niet met behulp van het framework geanalyseerd kunnen worden.

Deze bachelorproef bestaat uit verschillende delen. In een eerste deel werden verschillende nieuwe taalprimitieven, namelijk sin, cos, tan, sqrt en round, aan het framework toegevoegd, zodat nu ook programma’s die van deze primitieven gebruikmaken geanalyseerd kunnen worden. In een tweede deel werd een basisimplementatie voor quasiquoting aan het framework toegevoegd, een feature die onder andere voor het construeren van lijsten gebruikt wordt. In een derde deel werden bestaande Scheme-programma’s, die al dan niet reeds door SCALA-AM geanalyseerd kunnen worden, verzameld. Dit laat toe om een beeld te krijgen van welke niet-ondersteunde features het meest gebruikt worden, zodat de meest gebruikte features in de toekomst door SCALA-AM-ontwikkelaars ondersteund kunnen worden. Deze resultaten gaven aanleiding tot de uitbreiding van het eerste deel van de bachelorproef, waarin dan ook de append-primitieve geïmplementeerd werd.

De in deze bachelorproef geïmplementeerde features komen niet altijd overeen met de features die het meest gebruikt worden. Voor de implementatie van vele van deze meest gebruikte features is immers domeinspecifieke kennis omtrent abstracte interpretatie, de techniek die het framework gebruikt voor het analyseren van programma’s, nodig. Deze techniek valt echter buiten het bestek van de thesis. In plaats daarvan werd gefocust op veelgebruikte features die deze domeinkennis niet vereisen.

Tijdens de implementatie van append en quasiquoting werden enkele problemen vastgesteld die ervoor zorgden dat de implementatie van deze features bemoeilijkt werd, waardoor deze slechts deels geïmplementeerd werden. Deze problemen worden dan ook uitvoerig beschreven. De volledige implementatie van deze features valt buiten het bestek van deze bachelorproef, maar we bespreken wel, met aandacht voor alle potentiële complexiteiten, een mogelijke implementatie die als leidraad voor de verdere ontwikkeling van SCALA-AM gebruikt kan worden.

Het vervolg van dit verslag is als volgt gestructureerd: in hoofdstuk 1 geven we een overzicht van de structuur en werking van SCALA-AM. In hoofdstuk 2 beschrijven we hoe de nieuwe primitieven aan het framework toegevoegd werden, waarna in hoofdstuk 3 besproken wordt hoe quasiquoting toegevoegd werd. In hoofdstuk 4 worden de resultaten van het benchmarken toegelicht. Tot slot geven we in hoofdstuk 5 een algemene conclusie.

Publications

Van der Plas, J., Stiévenart, Q., & De Roover, C. (2025). Handling Cyclic Reinforcement of Lattice Values in Incremental Dependency-driven Static Analysis. In Proceedings of the 25th IEEE International Conference on Source Code Analysis & Manipulation (SCAM 2025).

Nowadays, many developers heavily rely on feedback from bug-detection tools to help ensure the quality of the code they produce. Such tools are underlain by static analysis. It is, however, critical for analysis results to be produced fast. To this end, incremental static analysis can be used. Upon a program change, an incremental analysis updates the previous results rather than recomputing the results from scratch.

Incremental static analyses may suffer from cyclic reinforcement of lattice values, where the computation of some values within the analysis relies on the values themselves, due to the abstractions made by the analysis. This can cause the incremental analysis to produce less precise results, reducing its usability.

In this work, we provide a solution to cyclic reinforcement of lattice values for incremental dependency-driven analyses. We compute the information flow within the analysis and show how this information flow can be used to detect cyclic reinforcements. We establish a criterion to detect when a cyclic reinforcement contains outdated information that needs to be removed, and show how precision can be regained. Our results show that using our method, an incremental analysis produces results matching a from-scratch analysis for all but one benchmark program, at the cost of a performance hit in some cases.

Verbelen, S., Vandenbogaerde, B., Van der Plas, J., Van Es, N., & De Roover, C. (2024). Abstract Slicing To Improve The Speed Of Static Program Analysis. In Proceedings of the 23rd Belgium-Netherlands Software Evolution Workshop (BENEVOL 2024).

When performing a static analysis, there is a trade-off between the time it takes to run the analysis and the quality of the results of the analysis. We propose to run the analysis on an abstract slice to reduce the size of the program to be analysed without impacting the results of the analysis. We adapt an abstract slicing algorithm to produce executable abstract slices that can be analysed using abstract interpretation. Next, we implement an intraprocedural abstract slicer for Scheme programs. We evaluate the implementation using a dataset of 1050 randomly generated Scheme programs. We find that abstract slices are in general smaller than their corresponding concrete slices and that in turn they are analysed faster. Additionally, we find that there is a significant difference between the abstract slices for two different abstract domains.

Wauters, C., Van der Plas, J., Stiévenart, Q., & De Roover, C. (2023). Change Pattern Detection for Optimising Incremental Static Analysis. In Proceedings of the 23rd IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2023) (pp. 49-60). IEEE. https://doi.org/10.1109/SCAM59687.2023.00016

Static analyses can be used by developers to compute properties of a program, enabling e.g., bug detection and program
verification. However, reanalysing a program from scratch upon every change is time-consuming, especially in settings where code changes often, such as within IDEs. To avoid such full reanalyses, incremental analyses instead reuse parts of the previous analysis result, and reanalyse the changed code as necessary.

While incrementality improves the analysis time, we introduce a complementary approach that further reduces the analysis
time. A traditional incremental analysis updates previous analysis results without domain-specific knowledge. However, the effect of particular source code changes on analysis results can be predicted. Performing a traditional incremental analysis of the changed code might therefore be unnecessary. Instead, we propose to detect code change patterns of which the effect on analysis results can be predicted and to update these results accordingly, saving potentially expensive computations.

In this paper, we explore the idea of adapting the analysis results for behaviour-preserving change patterns. In particular,
we consider consistent renamings, inverted conditionals, and moved function definitions within Scheme programs. We implemented our approach and evaluated it on 30 programs. We show decreases in incremental analysis time between 3% and 99% on 25 programs that contain at least one behaviour-preserving change pattern.

Van der Plas, J., Nicolay, J., De Meuter, W., & De Roover, C. (2023). ModInF: Exploiting Reified Computational Dependencies for Information Flow Analysis. In Proceedings of the 18th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2023). SCITEPRESS.

Information Flow Control is important for securing applications, primarily to preserve the confidentiality and integrity of applications and the data they process. Statically determining the flows of information for security purposes helps to secure applications early in the development pipeline. However, a sound and precise static analysis is difficult to scale. Modular static analysis is a technique for improving the scalability of static analysis. In this paper, we present an approach for constructing a modular static analysis for performing Information Flow Control for higher-order, imperative programs. A modular analysis requires information about data dependencies between modules. These dependencies arise as a result of information flows between modules, and therefore we piggy-back an Information Flow Control analysis on top of an existing modular analysis. Additionally, the resulting modular Information Flow Control analysis retains the benefits of its modular character. We validate our approach by performing an Information Flow Control analysis on 9 synthetic benchmark programs that contain both explicit and implicit information flows.

Van der Plas, J., Stiévenart, Q., De Roover, C. (2023). Result Invalidation for Incremental Modular Analyses. In: Dragoi, C., Emmi, M., Wang, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2023. Lecture Notes in Computer Science, vol 13881. Springer, Cham. https://doi.org/10.1007/978-3-031-24950-1_14

To reduce the running time of static analysis tools upon program changes, incremental static analyses reuse and update pre-existing results. Such analyses must efficiently detect and remove outdated results. We introduce three novel, complementary result invalidation strategies for incremental modular analyses. The core idea of our work is to alternate invalidation with computation. We apply our strategies to a recent, state-of-the-art incremental modular analysis that suffers from imprecision, and evaluate them on soundness, precision, and performance. Our strategies lead to precision improvements compared to an incremental analysis without invalidation, though the precision of a full reanalysis is not yet matched. On most benchmarks, our incremental analysis performs well. However, on some benchmarks our analysis performs poorly as the changes drastically change program behaviour, for which the changes are difficult for an incremental analysis to handle.

Kursun, T. R., Van der Plas, J., Stiévenart, Q., & De Roover, C. (2022). RacketLogger: Logging and Visualising Changes in DrRacket. In Proceedings of the 15th European Lisp Symposium ELSAA. https://doi.org/10.5281/zenodo.6326894

Developers frequently make code changes while programming, such as deleting a line of code and renaming or introducing a
variable. These changes can be detected and logged, for example by the IDE used by the developer. Logging changes is possible at two levels: at the textual level or at the level of the abstract syntax tree (AST) of the program. The logged changes, in both forms, are useful because they can be used to build new software engineering tools, such as static code analysers.

Plugins that log changes have already been developed for some IDEs. However, so far, no change-logging plugin has been developed for the DrRacket IDE, which supports the development of programs written in Scheme-like languages such as R5RS Scheme and Racket. To fill this gap, we have developed RacketLogger, a change-logging plugin for DrRacket. RacketLogger logs changes both at the textual level and at the AST level. To determine changes at the level of the AST, we have adapted Negara et al.’s algorithm to support Scheme syntax. We have evaluated our plugin by creating a visualisation for the logged changes to measure how well RacketLogger can be used as a building block, and conducted a small-scale user study to measure its usability.

Stiévenart, Q., Van Es, N., Van der Plas, J., & De Roover, C. (2021). A Parallel Worklist Algorithm and Its Exploration Heuristics for Static Modular Analyses. Journal of Systems and Software, 181. https://doi.org/10.1016/j.jss.2021.111042

One way to speed up static program analysis is to make use of today’s multi-core CPUs by parallelising the analysis. Existing work on parallel analysis usually targets traditional data-flow analyses for static, first-order languages such as C. Less attention has been given so far to the parallelisation of more general analyses that can also target dynamic, higher-order languages such as JavaScript. These are significantly more challenging to parallelise, as dependencies between analysis results are only discovered during the analysis itself. State-of-the-art parallel analyses for such languages are therefore usually limited, both in their applicability and performance gains.

In this work, we propose the parallelisation of modular analyses. Modular analyses compute different parts of the analysis in isolation of one another, and therefore offer inherent opportunities for parallelisation that have not been explored so far. In addition, they can be used to develop a general class of analysers for dynamic, higher-order languages. We present a parallel variant of the worklist algorithm that is used to drive such modular analyses. To further speed up its convergence, we show how this algorithm can exploit the monotonicity of the analysis. Existing modular analyses can be parallelised without additional effort by instead employing this parallel worklist algorithm. We demonstrate this for ModF, an inter-procedural modular analysis, and for ModConc, an inter-process modular analysis. For ModConc, we reveal an additional opportunity to exploit even more parallelism in the analysis: analyses of individual ModConc components can themselves be parallel, resulting in a doubly-parallel exploration. Finally, we present several heuristics for the exploration order of the analysis and discuss how they can impact its performance.

The parallel worklist algorithm and the exploration heuristics are implemented for and integrated into MAF, a framework for modular program analysis. On a set of Scheme benchmarks for ModF, we observe speedups between 3× and 8× when using 4 workers, and speedups between 8× and 32× when using 16 workers, with a maximum speedup of 333× using 128 workers. For ModConc, we achieve a maximum speedup of 37× with 32 workers. We observe that on a ModF analysis, among 11 exploration heuristics, the heuristics prioritising either components with smaller environments or with less dependencies result in consistent speedups that can reach 20× those of a random exploration strategy. We find a clear correlation between the mean number of dependencies in a program and the speedup obtained by this heuristic.

Van Es, N., Stiévenart, Q., Van der Plas, J., & De Roover, C. (2020). A Parallel Worklist Algorithm for Modular Analyses. In Proceedings of the 20th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2020) (pp. 1-12). IEEE. https://doi.org/10.1109/SCAM51674.2020.00006

Our parallel worklist algorithm is implemented and integrated into MAF, a framework for modular program analysis. Using a set of Scheme benchmarks for ModF, we usually observe speedups between 3× and 8× when using 4 workers, and speedups between 8× and 32× when using 16 workers. For ModConc, we achieve a maximum speedup of 15×.

Van der Plas, J., Stiévenart, Q., Van Es, N., & De Roover, C. (2020). Incremental Flow Analysis through Computational Dependency Reification. In Proceedings of the 20th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2020) (pp. 25-36). IEEE. https://doi.org/10.1109/SCAM51674.2020.00008

Static analyses are used to gain more confidence in changes made by developers. To be of most use, such analyses must deliver feedback fast. Therefore, incremental static analyses update previous results rather than entirely recompute them. This reduces the analysis time upon a program change, and makes the analysis well-suited for environments where the code base is frequently updated, such as in IDEs and CI pipelines.

In this work, we present a general approach to render a modular static analysis for highly dynamic programs incremental, by exploiting dependencies between intermediate analysis results. Modular analyses divide a program in interdependent parts that are analysed in isolation. The dependencies between these parts stem, for example, from the use of shared variables within the program. Our incrementalisation approach leverages the modularity of the analysis together with the dependencies that it reifies to compute and bound the impact of changes. This way, only the affected parts of the result need to be reanalysed, and unnecessary recomputations are avoided.

We apply our approach to both a function-modular and a thread-modular analysis and evaluate it by comparing an incremental update of an existing result to a full reanalysis. We find reductions of the analysis time from 6% to 99% on 14 out of 16 benchmark programs, and on most programs the impact on precision is limited. On 7 of the programs, reanalysis time is reduced by more than 75%, showing that our approach results in fast incremental updates.

Van Es, N., Van der Plas, J., Stiévenart, Q., & De Roover, C. (2020). MAF: A Framework for Modular Static Analysis of Higher-Order Languages. In Proceedings of the 20th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2020) (pp. 37-42). IEEE. https://doi.org/10.1109/SCAM51674.2020.00009

A modular static analysis decomposes a program’s analysis into analyses of its parts, or components. An inter-component analysis instructs an intra-component analysis to analyse each component independently of the others. Additional analyses are scheduled for newly discovered components, and for dependent components that need to account for newly discovered component information. Modular static analyses are scalable, can be tuned to a high precision, and support the analysis of programs that are highly dynamic, featuring e.g., higher-order functions or dynamically allocated processes.

In this paper, we present the engineering aspects of MAF, a static analysis framework for implementing modular analyses for higher-order languages. For any such modular analysis, the framework provides a reusable inter-component analysis and it suffices to implement its intra-component analysis. The intra-component analysis can be composed from several interdependent and reusable Scala traits. This design facilitates changing the analysed language, as well as the analysis precision with minimal effort. We illustrate the use of MAF through its instantiation for several different analyses of Scheme programs.