The date for the annual meeting of the IFIP WG 1.6 is Saturday, July 19, 2025. The meeting is co-located with FSCD 2025, and will take place on the first post-conference workshop day.
Abstract: Anti-unification (AU), also known as generalization, is a fundamental operation used for inductive inference. It is abstractly defined as a process deriving from a set of symbolic expressions a new symbolic expression possessing certain commonalities shared between its members. While most investigations focus on the first-order or equational variants, there have been a few developing algorithms for higher-order variants and investigating applications of existing procedures. Recent investigations focused on the simply-typed lambda calculus, but considering generalizations from fragments beyond patterns. In this talk, we discuss this recent work, open problems, and next steps to generalize the results to more expressive type systems of the lambda cube.
Abstract: NuITP is an inductive equational theorem prover for Maude equational theories that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms). Maude equational theories include expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms. This talks presents the tool, explains its most commonly used inference rules, and illustrates their use in proving the card trick benchmark.
Abstract: Traditionally, research on verification has a stronger focus on proving rather than disproving properties like termination or safety. While proving such properties requires over-approximations, under-approximating reasoning is needed to disprove them. Similarly, most techniques for worst-case complexity analysis are based on over-approximations and thus yield upper instead of lower bounds. In this talk, we survey various approaches for computing symbolic under-approximations for rewrite and transition systems that approximate reductions of arbitrary length, and give rise to state-of-the-art techniques for proving non-termination unsafety, and worst-case lower bounds.
Abstract: In the realm of term rewriting, given terms s and t, a reachability condition is said to be feasible if there exists a substitution such that s rewrites to t in zero or more steps; otherwise, it is called infeasible. Checking the infeasibility of (sequences of) reachability conditions is important in analyzing computational properties of rewrite systems, such as confluence or (operational) termination.
In this talk, we show how infeasibility can be introduced in the automatic analysis of computational properties of variants of term rewriting system. Furthermore, we present how a more general notion of feasibility enables more advanced analyses, allowing us to prove properties of more complex systems, such as Maude theories.
Abstract: Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and alpha-renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in alpha-equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the pi-calculus.
Joint work with Ali K. Caires-Santos and Maribel Fernández.
09:00--10:00: Session 1
10:30--12:30: Session 2
14:00--15:30: Session 3
16:00--17:00: Session 4
17:00--17:30: Business meeting (only for members)
The meetings of the working group are public, with the single exception of the business meeting. The presentations are all in-person, but will be livestreamed.
Cynthia Kop and Carsten Fuhs