Razborov's flag algebra forms a powerful framework for deriving asymptotic inequalities between induced subgraph densities, underpinning many advances in extremal graph theory. This survey introduces flag algebra to computer scientists working in logic, programming languages, automated verification, and formal methods. We take a logical perspective on flag algebra and present it in terms of syntax, semantics, and proof strategies, in a style closer to formal logic. One popular proof strategy derives valid inequalities by first proving inequalities in a labelled variant of flag algebra and then transferring them to the original unlabelled setting using the socalled downward operator. We explain this strategy in detail and highlight that its transfer mechanism relies on the notion of what we call an adjoint pair, reminiscent of Galois connections and categorical adjunctions, which appear frequently in work on automated verification and programming languages. Along the way, we work through representative examples, including Mantel's theorem and Goodman's bound on Ramsey multiplicity, to illustrate how mathematical arguments can be carried out symbolically in the flag algebra framework.
Can we use "hardness vs randomness" techniques to design low-space algorithms? This text surveys a sequence of recent works showing ways to do that. These works designed algorithms for certified derandomization and for catalytic computation (which work unconditionally), derandomization and isolation algorithms from remarkably mild assumptions, and "win-win" pairs of algorithms that, for every input, solve either derandomization or another important problem (e.g., s-t connectivity) on the input. Underlying these constructions are new, specialized "hardness vs randomness" tools for the setting of low-space algorithms. We describe these technical tools, most notably constructions of pseudorandom generators whose reconstruction algorithm (i.e., the security reduction) is a deterministic low-space algorithm. We also explain a key part of obtaining deterministic reconstruction, which is deterministic transformations of distinguishers to bit-predictors. We pose a host of open questions that explore new ways of using hardness vs randomness to design low-space algorithms. These questions address problems in derandomization, catalytic computation, explicit constructions, learning algorithms, and more.
We summarize the results of a 2024 survey of theory of computing (ToC) courses that received responses from 166 institutions of higher education in the United States [8]. Although our survey is far from comprehensive, it provides new information on many aspects of ToC in U.S. bachelor's degree programs in computer science. We report on the most frequently covered topics in ToC courses as well as structural features such as typical prerequisites, section sizes, teaching modalities, and course staff. In addition to summarizing survey results, we briefly discuss observed trends, suggest opportunities for future teaching and research, and conclude with a call for increased collaboration between American and European theoretical computer science educators.
This article surveys some of the work on the theoretical foundations of runtime monitoring carried out by various subsets of its authors over the last decade. It focuses on runtime monitoring of classic regular properties, of data-dependent properties and of hyperproperties. The paper also highlights the research philosophy guiding those studies, and the role that classic notions and techniques from concurrency theory have played in them.
Distributed computing is the science of cooperation. More precisely a distributed algorithm is composed of a set of computing entities (imposed to the programmers) each providing its own input, that have to cooperate to a common goal depending on the set of inputs (usually in the presence of adversaries such as asynchrony and failures) [2, 3]. . If follows that, in distributed computing, possibility/impossibility results and algorithmic techniques differ from what is encountered in sequential or parallel computing. This characterizes the distributed computing community. DISC and PODC are the very top conferences devoted to distributed computing.
Video talks, a staple of modern conferences and a great accessibility tool, are nonetheless maligned for being inferior versions of traditional live talks. We push back on this from two perspectives: first, that with clearer goals in mind video talks can be made to perform different functions than live talks; and second, that with basic editing video talks can be every bit as good as live talks, and can even reach creative heights unachievable in non-recorded settings. We make the case that creating such purposeful, engaging video talks is a benefit to the field, and should become more normalized therein.
Given a formula, what is the smallest number of variables with which it can be equivalently written? What seems like an abstruse question in syntactic manipulation turns out to have significance in a variety of areas of theoretical computer science. The number of variables in a formula emerges as an important measure related to notions of width arising in fields as varied as database theory; combinatorics and graph theory; and permutation groups. I explore how these notions are related to each other and the exploration will take us through a diverse landscape of topics, from comonads to lower bounds in circuit complexity.
This article addresses the question of whether concepts from formal logic can meaningfully contribute to mathematics education at the school level. We report on an attempt to work with high school teachers of mathematics in India on notions from logic such as: the notion of truth relative to a structure, construction of models for a set of sentences, consistency of procedures in algebra, and reasoning about algorithms used in school and comparing those algorithms systematically. Broadly, we tried to engage teachers in using ideas from logic to help with students' misconceptions, and to help students with reasoning about procedures.
Amnesiac Flooding [6, 7, 9] is the stateless/historyless/amnesiac variant of probably the oldest and simplest of distributed algorithms: (classic) flooding. Beginning with a message at a set of initiator(s), the algorithm at every node is simply a single rule: if the message is received from some neighbour(s), immediately forward it to the rest of the neighbours. Note that unlike classic flooding, no copy of the message or history of the flooding is retained to ensure termination/quiescence of the messages. Yet, surprisingly, amnesiac flooding begun from any set of initiators (even in differ-ent rounds) terminates on all undirected graphs in the synchronous message passing model. Moreover, it terminates in optimal rounds in bipartite graphs and is at most twice as slow in non-bipartite graphs. A series of results have followed the first discovery, improving our understanding of the process and its variants. Even more recently Austin, Gadouleau, Mertzios, and Trehan [3,5] discovered uniqueness-under certain reasonable conditions including statelessness, amnesiac flooding is the only algorithm that solves terminating broadcast! As algorithm designers, the study of lower bounds and impossibility results (no algorithm exists) is well established, but we are not aware of results concerning uniqueness or, in general, even a sensible notion of countability of solutions to problems. This article presents some of the fundamental and interesting results around amnesiac flooding from its discovery to the present while not being a comprehensive review of the area that the initial result has spawned.
Traditional Byzantine fault tolerant (BFT) state machine replication (SMR) protocols have a reputation of having poor performance despite decades of work in optimizing these protocols. Recently, a new family of protocols, DAG BFT, has been shown to have much higher throughput than traditional BFT protocols despite having higher communication complexity. This has attracted a lot of interest in improving DAG BFT protocols. This brief survey gives background on the foundational DAG BFT protocols and summarizes the techniques of state-of-the-art results. Finally, it concludes by highlighting avenues for future work.
Beside the four cardinal directions on a compass (North, East, South, West), there are more fine grained directions between them, such as NorthEast and EastNorthEast. They are formed by concatenating neighboring directions, but not arbitrarily: EastNorth and NorthEastEast are incorrect directions. We study the underlying (though not explicitly given) recursive naming procedure. As it turns out, these generalized directions on a compass are indeed unique and are formed by a tabled Lindenmayer system, usually used to describe cellular plant growth. As we show, deciding whether a given string actually forms a direction is solvable in linear time.
This dialog paper offers a preview and provides a foretaste of an upcoming work on the axiomatization of interactive classical algorithms. The modern notion of algorithm was elucidated in the 1930s-1950s. It was axiomatized a quarter of a century ago as the notion of "sequential algorithm"; we call it "classical algorithm" here. The axiomatization was used to show that for every classical algorithm there is a behaviorally equivalent abstract state machine. It was also used to prove the Church-Turing thesis as it has been understood by the logicians. Starting from the 1960s, the notion of algorithm has expanded - probabilistic algorithms, quantum algorithms, etc. - prompting introduction of a much more ambitious version of the Church-Turing thesis commonly known as the "physical thesis." We emphasize the difference between the two versions of the Church-Turing thesis and illustrate how nondeterministic and probabilistic algorithms can be viewed as classical algorithms with appropriate oracles. The same view applies to quantum circuit algorithms and many other classes of algorithms.
A recent line of work has investigated the complexity of explicit construction problems through the study of a search problem known as Range Avoidance: given as input a boolean circuit C : {0,1}(n )-> {0, 1}(n+1), find an element y is an element of {0, 1}(n+1) outside of its range. Analysis of this search problem and its variants has lead to several exciting new results in derandomization and circuit complexity. In this survey we give an overview of this nascent research direction and its connections to some old and fundamental questions in complexity theory.
I received my PhD in Computer Science on January 31, 2024, under a Joint PhD agreement between Gran Sasso Science Institute (L'Aquila, Italy) and Dalhousie University (Halifax, Canada). I was supervised by Travis Gagie, Nicola Prezza and Catia Trubiani. My PhD thesis, Data Compression Meets Automata Theory, was selected by the Italian Chapter of the EATCS for the Best PhD Thesis Award. The thesis introduces a new paradigm for studying regular languages, establishing a connection between classical results in automata theory, such as the powerset construction, and the most important data structures for solving pattern matching queries on compressed strings, such as the Burrows- Wheeler transform. The results and the open problems should be of interest to both the algorithmic community and the formal language theory community.
We present a proposal for increasing the accessibility of formal methods to the large number of students who could benefit from it but may not be well-served by traditional introductions. Several principles drive our design: a focus on computer systems as the target of study; immersing in applications before theory; building up from programming knowledge; and the breaking down of big transitions into smaller pieces. Concretely, we have created tools, educational materials, evaluation platforms, and more to implement these ideas. This paper describes our philosophy, learning objectives, and learning progression and provides pointers to our materials.
Automata over infinite objects are a well-established model with applications in logic and formal verification. Traditionally, acceptance in such automata is defined based on the set of states visited infinitely often during a run. However, there is a growing trend towards defining acceptance based on transitions rather than states. In this survey, we analyse the reasons for this shift and advocate using transition-based acceptance in the context of automata over infinite words. We present a collection of problems where the choice of formalism has a major impact and discuss the causes of these differences.
As large language models (LLMs) advance, their role in higher education, particularly in free-response problem-solving, requires careful examination. This study assesses the performance of GPT-4o and o1-preview under realistic educational conditions in an undergraduate algorithms course. Anonymous GPT-generated solutions to take-home exams were graded by teaching assistants unaware of their origin. Our analysis examines both coarse-grained performance (scores) and fine-grained reasoning quality (error patterns). Results show that GPT-4o consistently struggles, failing to reach the passing threshold, while o1-preview performs significantly better, surpassing the passing score and even exceeding the student median in certain exercises. However, both models exhibit issues with unjustified claims and misleading arguments. These findings highlight the need for robust assessment strategies and AI-aware grading policies in education.
Quantum advantage is well-established in centralized computing, where quantum algorithms can solve certain problems exponentially faster than classical ones. In the distributed setting, significant progress has been made in bandwidth-limited networks, where quantum distributed networks have shown computational advantages over classical counterparts. However, the potential of quantum computing in networks that are constrained only by large distances is not yet understood. We focus on the LOCAL model of computation (Linial, FOCS 1987), a distributed computational model where computational power and communication bandwidth are unconstrained, and its quantum generalization. In this brief survey, we summarize recent progress on the quantum-LOCAL model outlining its limitations with respect to its classical counterpart: we discuss emerging techniques, and highlight open research questions that could guide future efforts in the field.
