Student Projects

Algebraic Effects is a formal system for describing and programming with side-effects in functional programming. They generalize a large class of familiar effects (like I/O, exceptions, mutable state), while allowing for compositional and modular programming and reasoning. In the paradigm of algebraic effects, specific side effects can be encoded using algebraic abstractions (hence the name) and treated as first-class objects with the use of handlers. While originating in theoretical computer science, algebraic effects have been implemented most notably as part of the latest release of the OCaml programming language, where they are used for the implementation of the concurrent subsystem. The goal of this project is to study both the theoretical foundations of algebraic effects, as well as the practice of programming with algebraic effects in OCaml. To this end, the student is to investigate the mathematical foundations of algebraic effects, and report on how it is connected with the practice of programming. At the end the student is expected to provide a report, which can serve as a guide to algebraic effects for fellow students who might be interested in the topic, as well as a collection of examples written in OCaml. Some relevant reading:

• An Introduction to Algebraic Effects and Handlers
• Programming with Algebraic Effects and Handlers
• OCaml Language Manual: Effect Handlers
• Effective Programming: Adding an Effect System to OCaml
• Friendship ended with Monads: Testing out Algebraic effects in OCaml for Animations
• What is algebraic about algebraic effects and handlers?

FitchVIZIER is a proof checker for Fitch-style proofs written in Rust and used in the course “Introduction to Logic” in the CS and AI programs. This project concerns possible improvements and extensions, raging from mostly practical to mostly theoretical. The idea is the during the course of this bachelor project you will study the topic from the theoretical point of view and implement it in FitchVIZIER. Given the context, this project is suitable for students who are interested and have some experience with logic and Rust. Potential improvements/extensions are:

• Support for external theorems and a module system
• An implementaiton of proofs by induction and unification
• Support for “partial” proofs
• Conversaion between Fitch-style and Gentzen-style proof systems

The aim of this project is to build a formally verified correct software, and to familiarize yourself with the Rocq system. Rocq is a proof assistant and a programming language, which allows the user not only to write and execute functional programs, but also to prove properties about them.

In the first part of this programming project the student will first familiarize themselves with the basics of Rocq. In the second part, the student will pick an algorithm or a data structure – for example, a queue, a look-up table, a binary tree, etc – and they will implement and verify it.

Required skills: Knowledge of functional programming and mathematical induction

Here are some more links that contextualize the project:

• Introduction to the Coq proof-assistant for practical software verification
• A book on Verified Functinal Algorithms
• See also the previous student projects on this topic.

Gradual typing bridges the gap between fully static typing (in languages like Java or Haskell) and fully dynamic languages (like Python or JavaScript), by allowing the programmer to mix typed and untyped code in the same project (similar to the TypeScript approach). This additional flexebility allows programmers to develop the programs in a dynamically-typed programming language and add type annotations to some crucial parts wihle leaving other parts untyped. It is precisely the interaction between the typed and untyped parts of the code that raises an important question: what kind of guarantees does a gradually typed program provide? Intuitively, we want to say that if a gradually typed program raises a type error, than that type error has to come from an untyped part. But what does this mean specifically? In presnse of higher-order constructs like first-class functions or objects it is suprisingly tricky to formulate this precisely. In this project you will investigate both theoretical and practical aspects of grdual typing, including imporant concepts like cast semantics, implicing casting, and the blame tracking. The project is suitable for people interested in type systems, as they are covered in classes on functional programming, compiler construction, and semantics.

Primary reading:

• What is Gradual Typing?
• Gradual Typing for Functional Languages
• Gradual Typing for Objects

This project is about implementing a type system for a programming language. A type system determines which programs in a programming language are valid, and which ones are not. A type system for example can reject a program that adds a number and a string together, thus catching a type error. And more advanced type system can catch more errors. The process of enforcing such a typing discipline is called type checking: given a program, annotated with types, a compiler checks whether to accept the program or reject it.

The natural question for implementers of compilers is then how to implement a type system, without requiring too much input from the user. That is, given a partially annotated program, can we infer the types? This is referred to as type inference.

One class of algorithms for implementing type systems are based on bidirectional type checking, which combines type checking and type inference into a straightforward algorithm.

The goal of this project is to study bidirectional type checking and implementing one of the algorithms in your favorite programming language. If you enjoyed the courses on functional programming or the elective course on compiler construction and semantics, then this project might be for you!

Additional reading:

• Bidirectional Typing Rules: A Tutorial, and
• Lecture Notes on Bidirectional Typechecking

Modal logic is an extension of propositional logic which can express properties of nondeterministic programs whose behaviour can be viewed as a transition system where states are variable assignments and the transition relation models the execution of instructions. For example, a formula ◊φ says that there is a transition to a state in which formula φ holds, and a formula Fφ says that there is a reachable state in which φ holds. Reachable states (including the current state) are sometimes called future states and we therefore refer to F as the future modality. F is a so-called fixpoint modality since it satisfies the equation Fφ = φ ∨ ◊Fφ (i.e. Fφ holds if and only if φ holds now or there is a transition to a state where Fφ holds).

The paper [1] presents a cyclic proof system GKe (with a cut-rule) for the modal logic with ◊ and F, and a cut-elimination procedure for this system. Cyclic proof systems are a form of sequent calculi that are particularly suited for logics with fixpoint modalities. Cyclic proofs have finite representations as labelled trees, but they are viewed as trees with back edges, or in other words, cyclic structures. The cut-rule and the significance of cut-elimination are fundamental to proof theory and its connection to the theory of computation, see e.g. [2] for a compact introduction. Cut-elimination in cyclic proofs poses added challenges due to the cyclic structure.

The aim of this project will be to implement the cut-elimination procedure for the cyclic proof system GKe, and analyse its complexity. It is part of the project to select a suitable programming language/platform. Options include Rascal [3], the Cyclist prover framework [4], or a high-level language like Haskell. For earlier student projects that used Rascal to implement formal proofs, see [5-6]. To carry out this project, the student would need to study paper [1] in detail and construct cyclic proofs that can be used as input for the cut-elimination procedure. This project is therefore suited for students who have a strong interest in logic.

References:

1. Bahareh Afshari and Johannes Kloibhofer. Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic. Proceedings of Fixpoints in Computer Science, 2024 [link]
2. Abhishek De and Iris van der Giessen. Introduction to Proof Theory. Lecture notes for Midlands Graduate School 2024 [link]
3. Paul Klint, Tijs van der Storm, and Jurgen Vinju. Rascal: A domain specific language for source code analysis and manipulation. Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, 2009 [link]. Rascal website.
4. James Brotherston, Nikos Gorogiannis and Rasmus L. Petersen. A Generic Cyclic Theorem Prover. Proceedings of APLAS 2012 [link]. Also available here. Cyclist Prover website.
5. Chris Worthington. Proof Transformations for Game Logic. BSc thesis, Computing Science, UG, 2021 [link]
6. Steven J. van Schagen. Game Logic: A Proof Transformation from Gentzen to Hilbert. BSc Thesis, Computing Science, UG, 2022 [link]

In real-world decision-making, multiple actors often have to make decisions on multiple issues at the same time. In the presence of multiple issues and multiple actors with varying preferences, there is rarely one outcome that is optimal for all actors. Moreover, preferences over outcomes for an issue A may depend on the outcomes of other issues B and C. For single actors, such conditional preferences have been formalized with conditional preference networks (CP-nets) [1]. Multi-actor extensions and other generalizations have been studied in [2,3].

The aim of this project is to create a web-based tool that will support real-world case studies in complex decision-making using multi-actor CP-nets. The tool should (1) provide an interface for querying users (actors) for input that will be used to construct a CP-net, and (2) compute a number of aggregation metrics that can help identify outcomes that optimize various aspects of the group’s preferences .

Re (1): In the worst case, a CP-net specification requires a number of queries that is exponential in the number of issues, but in most (real-world) cases, the specification is much smaller due to few dependencies. Therefore the user input process should consist of a number of steps that allow to minimize the number of queries to the user. Moreover, the CP-net specifications should be stored in a database, and allow for some basic visualization of CP-nets.

It is part of the project to identify a suitable programming language and the setup for the web tool. Students can get access to descriptions of issues and CP-nets from a real-world case study.

The main references are [2] and [3]. Reference [1] (sections 1 and 2) can be consulted for more details and motivation.

References:

1. Boutilier C, Brafman RI, Domshlak C, Hoos HH, Poole D (2004) CP-nets: A tool for representing and reasoning with conditional ceteris paribus preference statements. J. Artif. Intell. Res. 21:135–191 [link]
2. Rossi, F., Venable, K. B., and Walsh, T. (2004). mCP nets: Representing and reasoning with preferences of multiple agents. In AAAI, volume 4, pages 729–734 [link]
3. Haret, A., Novaro, A., & Grandi, U. (2018). Preference Aggregation with Incomplete CP-Nets. In 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018) (pp. 308-317). AAAI Press, Palo Alto, California [link]

The Covering by Arithmetic Progression problem asks: given a set of natural numbers, what is the smallest number of arithmetic progressions needed to cover all elements? This problem arises naturally in timetabling and scheduling/ For more details, see the recent article: “Covering by Arithmetic Progressions”.

Project Overview

• Bring known algorithms to life by coding them up.
• Test their performance on a variety of input data.
• Propose and develop heuristics to improve efficiency.
• Assess the practical effectiveness of your solutions.

Why This Project? This project is ideal for anyone fascinated by financial markets and interested in testing quantitative trading strategies. Price reversion—also known as mean reversion—is a classic approach used by traders to capitalize on short-term price fluctuations.

What You’ll Do You’ll investigate the effectiveness of a simple price reversion strategy, which operates on the following principles:

• Buy stocks that have decreased in value compared to their price one week ago.
• Sell or short stocks that have increased in value compared to their price one week ago.

Key Activities

• Data Collection: Scrape or source historical market data in a format suitable for analysis.
• Market Simulation: Model historical market conditions to test the strategy’s performance.
• Strategy Analysis: Evaluate the effectiveness and risks of basic price-reversion approaches.

Who Is This For? Are you a fan of football, basketball, volleyball, or any other popular sport? Do you enjoy analyzing game outcomes from a mathematical or computational perspective? If so, this project is for you.

Inspiration & Motivation This project is inspired by the article: “How to Make Knockout Tournaments More Popular?” (Juhi Chaudhary, Hendrik Molter, and Meirav Zehavi). The article raises fascinating questions about tournament design and optimization.

What You’ll Explore

• Tournament Optimization: How can we organize games (e.g., for the FA Cup) to maximize revenue, using data from previous seasons (such as the Premier League or other leagues)?
• Generalization: Can these insights be applied to tournaments in other countries or sports?
• Predictability: How predictable are results in certain sports leagues? Can we efficiently compute such predictions in general?

Project Goals Investigate the practical application of theoretical results from the article. Analyze real-world data to assess the predictability of tournament outcomes. Develop or adapt computational models to optimize tournament structures.

The chromatic number is a classic NP-complete problem: given a graph, what’s the minimum number of colors needed to color its vertices so that no two adjacent vertices share the same color? This question is deeply connected to the famous Four Color Theorem. List coloring and choosability are intriguing generalizations of this problem, offering rich avenues for research.

What You’ll Do: In this project, you’ll dive into the world of graph coloring, with a focus on:

• Surveying Known Results: Review and synthesize existing literature on chromatic number, list coloring, and choosability.
• Testing Hypotheses: Investigate open questions, such as: Is it true that any 3-choosable graph is (6,2)-choosable? (see this video)
• Empirical Exploration: Test hypotheses on small graphs or within specific graph classes, potentially uncovering new patterns or counterexamples.

Graphs are the backbone of computer science, and they are everywhere! They are used to model a wide variety of real-world problems, including social networks, transportation networks, and communication networks. Graphs have many parameters that describe their complexity and structure, and these parameters can be used to gain insights into the underlying problem. The simplest such parameters are the number of vertices and the number of edges, but there are more involved parameters like treewidth. This parameter describes how significantly a graph is different from a tree (more details can be found here: https://en.wikipedia.org/wiki/Treewidth). There are many other parameters like pathwidth, cliquewidth, twinwidth, vertex cover, neighborhood diversity, and so on. All these parameters can be used to gain a deeper understanding of how hard a particular problem is on a given graph. The goal of the proposed project is to investigate how LLMs are good in finding values of such parameters on small graphs. If you want to know more about treewidth you can watch the following video https://www.youtube.com/watch?v=kEnDGTwSDXY (understanding all material in the video is NOT necessary)

Who Is This For? This project is perfect for students passionate about graph theory, algorithms, or computational complexity. If you’re intrigued by the challenge of tackling NP-complete problems and discovering clever algorithmic solutions, this is your opportunity to dive deep.

Project Overview You’ll explore classical graph-based NP-complete problems, as cataloged in the seminal work: “Computers and Intractability: A Guide to the Theory of NP-Completeness” by Michael Garey and David S. Johnson.

Key Activities

• Identify graph problems from the book that can be solved faster than brute force.
• Investigate existing algorithms in the literature, or design your own innovative approaches.
• Describe, simplify, or enhance these algorithms, contributing to the understanding of efficient solutions for NP-complete problems. By the end of the project, you’ll have a comprehensive survey of graph problems with non-trivial algorithmic solutions, potentially uncovering new insights or optimizations

Who Is This For? This project is perfect for students passionate about algorithms, or computational complexity. If you’re intrigued by the challenge of tackling NP-complete problems and discovering clever algorithmic solutions, this is your opportunity to dive deep.

Project Overview You’ll explore classical non-graph-based NP-complete problems, as cataloged in the seminal work: “Computers and Intractability: A Guide to the Theory of NP-Completeness” by Michael Garey and David S. Johnson.

Key Activities

• Identify non-graph problems from the book that can be solved faster than brute force.
• Investigate existing algorithms in the literature, or design your own innovative approaches.
• Describe, simplify, or enhance these algorithms, contributing to the understanding of efficient solutions for NP-complete problems.

The Partial Minimum Satisfiability problem involves a CNF formula F, where some of the clauses are marked as hard clauses. The goal is to find a satisfying assignment that satisfies all hard clauses and the smallest number of other clauses. The length of the formula is defined as the number of literals in the formula. The objective of this project is to construct an algorithm for the Partial Minimum Satisfiability problem, with the running time measured in terms of the length of the formula or in terms of the overall number of variables and clauses. The algorithm will most likely be a branch-and-bound algorithm. You can find details about branching algorithms in Chapter 2 of the book Exact Exponential Algorithms. This project will introduce you to exact exponential algorithms and basic techniques for designing such algorithms. You will also have the opportunity to construct your own algorithm for the Partial Minimum Satisfiability problem. Good luck!

Literature:

• Exact Exponential Algorithms
• Description of the Partial Minimum Satisfiability problem and its applications.

This project concerns formal languages able to express concurrency, in the form of processes that execute simultaneously and interact with each other by exchanging messages. We are particularly interested in message-passing processes that follow a client-server architecture, where client processes send a message to invoke some server process that provides some useful functionality and is always available. This kind of client-server interaction is very common in practice, and it is important to have precise tools to reason about the correct behavior of clients and servers.

Interestingly, logic can provide a precise setting to reason about clients, servers, and their intended interactions. This project concerns linear logic, a type of logic that tracks resources used by processes, in which client-server interactions can be neatly represented. There are several seemingly related logical characterizations of client-server interactions using linear logic; the goal of this project is to study the most important characterizations and to compare their most relevant characteristics by means of examples.

In this project you will learn about models of concurrency, static verification (type systems), and the Curry-Howard correspondence: a beautiful connection between static verification and logic. See https://www.jperez.nl/teaching/projects for a list of suggested pointers.

Deliverables: A written report, in the style of a scientific paper, that surveys in a self-contained manner different characterizations of client-sever interactions using linear logic.

This project concerns formal languages able to express concurrency, in the form of processes that execute simultaneously and interact with each other by exchanging messages. In particular, we are interested in APCP, a formal language in which message-passing processes implement protocols. In prior research, we have determined the formal conditions under which programs in APCP execute their protocols without running into a deadlock: the situation in which a program is stuck waiting for a message that will never arrive. We have used linear logic, a type of logic that tracks resources used by APCP processes, to ensure freedom from deadlocks.

We have already demonstrated the power of APCP in different scenarios that involve concurrency. The goal of this project is to complement this work by developing an APCP program that implements a solution to Dijkstra’s Dining Philosophers problem, one of the most famous problems in concurrent programming. Concretely, in this project you will use APCP to implement a solution to the problem based on a resource hierarchy. That is, you will develop an implementation of the dining philosophers that exploits concurrent synchronizations and prove that it never runs into deadlocks.

In this project you will learn about models of concurrency, static verification (type systems), and the Curry-Howard correspondence: a beautiful connection between static verification and logic. See https://www.jperez.nl/teaching/projects for a list of suggested pointers.

Deliverables: A written report, in the style of a scientific paper, that presents your verified implementation of the Dining Philosophers problem in APCP.

This project concerns formal languages able to express concurrency, in the form of processes that execute simultaneously and interact with each other by exchanging messages. In particular, we are interested in APCP, a formal language in which message-passing processes implement protocols. These protocols are specified using session types, which describe structures of intended communication. Communication in APCP is asynchronous: a data structure called buffers is used to store messages that have been sent but not yet received.

Prior work by Gay and Vasconcelos (for a language similar to APCP) showed that one can obtain an upper bound on the necessary size of the buffers (see here). Intuitively, the idea is to examine the intended protocol, and to derive an upper bound for a buffer using the protocol’s size. This informally means that a protocol with n message exchanges will require a larger buffer than the one needed to implement a protocol with k message exchanges, for any k < n. The goal of this project is to adapt the argument by Gay and Vasconcelos to the case of APCP. This entails studying the definitions and proofs by Gay and Vasconcelos and to check whether/how they apply to the case of APCP, in which session types are closely related to linear logic, a type of logic that tracks resources used by processes.

In this project you will learn about models of concurrency, static verification (type systems), and the Curry-Howard correspondence: a beautiful connection between static verification and logic. See https://www.jperez.nl/teaching/projects for a list of suggested pointers.

Deliverables: A written report, in the style of a scientific paper, that presents your formal analysis (definitions and proofs) for the upper bound of buffers in APCP.

A fundamental task in logic and theoretical computer science is to understand the computational difficulty of logical decision problems such as satisfiability, validity, and provability. These difficulties are usually established via reductions from hard computational problems. Depending on the problem under consideration, the reduction yields either a computational complexity lower bound, or undecidability.

The aim of this project is to survey reduction-based lower bounding techniques for non-classical logics, including substructural, intermediate, and modal logics. In each case, one starts from a computational problem whose difficulty is known, and encodes its computations into a logical system.

The aim of this project is to survey and illustrate key reduction techniques used in the study of non-classical logics, with a focus on:

• Substructural logics (e.g. fragments of linear and relevant logic)
• Intermediate logics (between intuitionistic and classical logic)
• Modal logics.

The project will examine how well-known hard problems—such as counter machine reachability, tiling problems, and quantified Boolean formulas—are reduced to logical decision problems. Particular emphasis will be placed on clearly explaining:

• the computational problem used for the reduction
• the logical system under study
• how the problem is encoded in the logic (i.e., the reduction)

Case studies include:

• Counter machine encodings used to obtain undecidability and lower bounds for linear logic and fragments of substructural logics,
• Reductions from TQBF establishing PSPACE-hardness for intuitionistic propositional logic,
• Wang tiling–based arguments yielding hardness and undecidability results for relevant and modal logics.

The aim of this project is primarily expository: the student is not expected to prove new results, but to find suitable examples from the literature and present the arguments in a clear, accessible and systematic way, suitable for a reader with a background in logic and basic complexity theory. Additional topics to consider include a comparison of reduction techniques across different logical families, highlighting common patterns and differences; a focused case study on a single technique (e.g., counter machines or tilings) applied to several logics; an exploration of how lower bounds rely on properties of the logical proof system such as cut-elimination or subformula properties; and a brief discussion of open problems or gaps between known upper and lower bounds in specific logics. Depending on progress and interest, there may be scope to consider a research problem.

This project can be seen as complementary to The Computational Origins of Hardness for Canonical Problems. While the present project studies how hard problems can be encoded into logical systems to obtain lower bounds and undecidability results, the companion project examines why these problems are hard, in terms of Turing machine computation.

This project is suitable for a student with an interest in the mathematical and theoretical foundations of computer science, particularly logic and complexity theory. Familiarity with propositional logic and computational complexity is assumed; prior exposure to non-classical logics is helpful but not required.The project is suitable for two students, who could divide the work between surveying complexity-theoretic lower bounds and surveying undecidability results, unified by a common focus on reductions from hard problems.

References:

• Richard Statman: Intuitionistic Propositional Logic is Polynomial-Space Complete. Theor. Comput. Sci. 9: 67-72 (1979)
• Alasdair Urquhart: The Complexity of Decision Procedures In Relevance Logic II. J. Symb. Log. 64(4): 1774-1802 (1999)

Many lower-bound and undecidability results rely on a small collection of canonical computational problems whose difficulty is well understood. These problems are rarely arbitrary: they are carefully chosen abstractions of Turing machine computation, designed to preserve hardness while offering structures that are easier to manipulate and encode. This project focuses on understanding the computability/complexity properties of these source problems.

The project will survey several foundational hard problems that commonly serve as starting points for reductions, including:

• the Halting Problem and related undecidable decision problems for Turing machines
• bounded Turing machine problems corresponding to standard complexity classes (in particular polynomial-space computation)
• intermediate computational models such as counter machines, tiling systems, and string or term rewriting systems

For each case, the aim is to explain

• the underlying computational model and how it relates to Turing machines,
• how hardness or undecidability is established (without using prior reductions),
• why the problem is a convenient and robust source for further reductions, and
• how it connects to other canonical hard problems via simple simulations or reductions.

The central goal of the project is to make explicit the computational lineage of lower-bound arguments: how undecidability and high complexity originate in Turing machine behaviour, and how this difficulty is preserved as one moves to higher-level or more structured problems. Particular attention should be paid to why certain problems—such as tiling or counter machines—are often preferred over Turing machines when serving as reduction sources. The student is expected to search the literature for relevant sources. The aim of this project is primarily expository: the student is not expected to prove new results.

This project can be seen as complementary to the project Reduction-Based Lower Bounds and Undecidability in Logic. While the latter studies how computational hardness is encoded within logical systems, the present project focuses on the computational origins of that hardness and on the role of Turing machines as the foundational reference model.

This project is suitable for a student interested in theoretical computer science and models of computation. Familiarity with Turing machines, decidability, and computational complexity is assumed.

As energy efficiency has become a crucial concern, a new design paradigm called Approximate Computing (AC) has gained popularity. While traditionally one could sacrifice latency for energy efficiency, AC proposes to consider accuracy as a design axis, aiming to lower energy consumption at the cost of accuracy. This is well suited for error-resilient applications, where small losses in accuracy are not critical.

This project will focus on the design of boolean circuits via Approximate Logic Synthesis (ALS) [1]. ALS is the process of automatically generating an approximate version of a circuit that respects an error threshold. The resulting circuit will be a modification of the original one, with parts substituted or even completely removed, and should have improvements in metrics such as energy consumption. Recent advances on ALS have exploited Satisfiability Modulo Theories (SMT) solvers [2]. These solvers provide heuristics to tackle the SMT problem [3], which is a generalisation of Boolean Satisfiability (SAT), the quintessential NP-complete problem.

The aim of the project is to investigate improvements to the SMT-based approach described in [2], e.g., in terms of subcircuit selection and encoding. You will need a suitable understanding of logic and basic knowledge of gate-level design, in addition to good programming skills. The tasks will include (a) learning about one step of the framework, by reading the academic paper and the framework’s documentation and codebase, (b) designing an alternative approach to complete the step, and (c) implementing the new approach in an experimental branch of the framework.

The framework is implemented in Python and can be found on GitHub: https://github.com/lp-rg/subxpat

References:

• [1] I. Scarabottolo, G. Ansaloni, G. Constantinides, L. Pozzi, and S. Reda. Approximate Logic Synthesis: A Survey. Proceedings of the IEEE (Proc. IEEE), volume 108, issue 12, 2020. DOI: https://doi.org/10.1109/JPROC.2020.3014430
• [2] M. Rezaalipour, M. Biasion, F. Costa, C. Tirelli, F. Ferretti, R. Otoni, G. Constantinides, and L. Pozzi. Approximate Logic Synthesis via Iterative SMT-based Subcircuit Rewriting. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Early Access, 2025. DOI: https://doi.org/10.1109/TCAD.2025.3638267
• [3] C. Barrett, C. Tinelli, H. Barbosa, A. Niemetz, M. Preiner, A. Reynolds, and Y. Zohar. Satisfiability Modulo Theories: A Beginner’s Tutorial. Proceedings of the 26th International Symposium on Formal Methods (FM’24), 2024. DOI: https://doi.org/10.1007/978-3-031-71177-0_31