Embedded finite model theory refers to a formalism for describing finite structures over an uninterpreted signature, which sit within an infinite interpreted structures. Some theory was developed in the 1990’s and early 2000’s, with a focus on the real field. But the theory applies to arbitrary theories, and is relevant to recent development on graph querying and analysis of data-driven programs involving arithmetic.

In this invited paper we review the framework and some of the basic results on it. We also discuss some open questions, along with some work in progress, joint with Ehud Hrushovski.

In this short survey we describe recent advances on the Post Correspondence Problem in group theory that were inspired by results in computer science. These algebraic advances can, in return, provide a source of interesting problems in more applied, computational settings.

Post’s Correspondence Problem (PCP) is a classical decision problem in theoretical computer science that asks whether for a pair of free monoid morphisms g,h : Σ^*→ Δ^* there is any x ∈ Σ^* such that g(x) = h(x). One can similarly phrase a PCP for general groups, rather than free monoids, by asking whether pairs g,h of group homomorphisms agree on any inputs. This leads to interesting and unexpected (un)decidability results for PCP in groups.

Automated analysis of multithreaded shared memory programs is a core problem in verification. While the general verification problem for these systems is undecidable, already when there are only two recursive threads, there has been a lot of work to find appropriate underapproximations. Context-bounding is one such underapproximation technique. In context bounded analysis, we set an a priori bound K and restrict attention to only those runs of the system in which each thread is interrupted at most K times. It turns out that many verification problems become decidable under the restriction of context bounding. In this talk, I will provide a survey of recent results in this area. Specifically, we shall consider context-bounded safety and liveness verification for systems in which threads can spawn new threads, as well as practically-motivated restrictions of the problem such as thread pooling. (Joint work with Pascal Baumann, Moses Ganardi, Ramanathan Thinniyam, and Georg Zetzsche.)

This paper surveys results that establish formal connections and distinctions between SAT-based invariant inference and exact concept learning with queries, showing that learning techniques and algorithms can clarify foundational questions, illuminate existing algorithms, and suggest new directions for efficient invariant inference.