Program for CICM 2025

TBA

Auditorium CIC/EST

TBA

Auditorium CIC/EST

Maintaining large formal mathematics libraries is labor intensive. We propose methods to reduce this effort by exploiting structural similarity: First, we detect duplicates by combining syntax, markup, and formula structure, using a scalable discriminator-based approach that achieves perfect precision on Isabelle/HOL up to a 0.95 similarity threshold. Second, we identify proper locations for auxiliary lemmas via community detection on dependency graphs, suggesting the correct location within the top 6 neighborhoods on average (median).

TBA

Auditorium CIC/EST

Several successful analysis tools and platforms support compositional verification and/or compositional bug-finding for heap-manipulating programs. These approaches are often powered by compositional symbolic execution (CSE), grounded in ideas from separation logic (SL) and incorrectness separation logic (ISL). In this context, “compositional” means that the analysis scales by reasoning about functions in isolation—anywhere in the codebase—producing simple function specifications that can be reused in broader calling contexts. Modern CSE-based tools rely critically on two capabilities: reasoning about function calls using function specifications, and manipulating user-defined predicates. A key challenge that arises here is the frame inference problem (FIP): determining which parts of the symbolic state are relevant for a given operation. Many tools address FIP using a consume-produce approach, which reduces the problem to a form of matching between logical assertions and symbolic states. In this talk, I will argue that the FIP—and, more broadly, symbolic analysis in this setting—is inherently an equational problem. Reasoning modulo axioms, while often necessary, introduces a significant burden that must be carefully managed in both the formalisation and implementation of these analyses (Joint work with Andreas Lööw, Philippa Gardner and Simon Park).

TBA

Auditorium CIC/EST

Symbolic constraint solving is a fundamental technique in many areas of mathematics and computer science, providing the basis for key operations in automated reasoning, term rewriting, declarative programming, or formal methods. Important classes of symbolic constraints include unification, matching, generalization, disunification, ordering constraints. Efficient methods for solving them form the computational core of inference engines, proof assistants, program transformation systems, logical frameworks, etc. In this talk, we present recent advances in solving unification, matching, and generalization constraints in expressive theories, including those that involve background knowledge or binding constructs. We discuss algorithmic techniques for constraint solving, identify classes of problems that admit efficient solutions, and highlight their relevance for tools and techniques in symbolic computation and computer mathematics.

TBA

Auditorium CIC/EST

Theory combination in Satisfiability Modulo Theories (SMT) deals with the generation of algorithms for combinations of theories, based on the algorithms for each of the specific theories being combined. Among the most important combination methods is the polite combination method, which has two major advantages: first, it only requires solvers for the theories being combined, and no other mechanism is needed (e.g., there is no need for an algorithm that computes cardinalities of models). Second, it only requires one of the theories to admit some property, while the other only has to be decidable. When polite combination was introduced, it was claimed that the required property is "politeness" (a notion I will formally and intuitively describe in my talk). But, later, it was shown that the correctness proof had a bug, and for the proof to work, a stronger property is needed to be assumed, namely "strong politeness". Hence, while the importance of the polite combination method is unquestionable (its incorporation in the state-of-the-art solver cvc5 is a case in point), it was left unclear what is the value of the politeness property. Can it still be considered a property that is relevant to theory combination? In this talk I will describe several attempts made by myself and others to answer this question positively, thus saving the politeness property. No background in theory combination or SMT is assumed, though politeness is expected.

TBA

Auditorium CIC/EST

Propositional Dynamic Logic (PDL) is a sophisticated modal logic tailored to reason about programs. Several fragments and extensions of PDL are worth studying, allowing us to control complexity or increase expressiveness. By limiting PDL to deterministic fragments, such as Deterministic PDL or Strictly Deterministic PDL, we introduce new program behaviors by excluding nondeterministic choices or restricting the form of iteration. These restrictions affect both expressiveness and computational complexity. While standard PDL is decidable and has an EXPTIME-complete satisfiability, some deterministic fragments have lower complexity bounds, such as PSPACE-complete. It is a showcase of a trade-off between expressiveness and tractability. Conversely, attempts to increase expressiveness come with significant challenges. Extensions like Context-Free PDL result in undecidable validity. This discussion will explore the effects of restricting to deterministic programs and examine how to enhance expressiveness using memory.

TBA

Auditorium CIC/EST