ABSTRACT. Rewriting induction is a form of inductive theorem proving to show that two terms in a term rewriting system compute the same value. This is a basic, easily understandable proof system -- for term rewriting systems. But what if we want to use it on functional programs? We can deal with in-built data structures like integers, but once we encounter higher-order variables -- a staple in any functional language -- new questions arise. Questions such as "what does equivalence even mean?" and "can I analyse these two tiny functions without knowing the entire program around it?" and "okay, but does this ever work for actually practical questions?". In this talk, I will discuss some possible answers to these questions, and show how we can use rewriting induction in general to analyse simple functional programs.

ABSTRACT. Contextual equivalence is the standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction. In the paradigmatic case of the untyped 𝝺-calculus, the talk will introduce _interaction equivalence_ (recent work published in POPL 2025). Inspired by game semantics, we observe the number of interaction steps between terms and contexts but---crucially---ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as ℬ, the well-known theory induced by Böhm tree equality. It is the first observational characterization of ℬ obtained without enriching the discriminating power of contexts with extra features such as non-determinism.

ABSTRACT. Program equivalence is a notoriously undecidable problem, consequently, all approaches to determining whether two programs are equivalent are either imprecise or labor-intensive. In practical applications, developers often rely on proxy measures, such as the syntactic similarity of programs. In this paper, we formalize what it means for a similarity measure to be semantically descriptive and provide a framework for ranking measures based on their ability to differentiate between equivalent and non-equivalent program pairs. We refer to this metric as the average semantic loss of the similarity measure. We evaluate 17 established similarity measures, including those based on edit distance, compression, and vector embeddings. Using a subset of 0.45 million program pairs from the IBM ProjectCodeNet benchmark, we show that our semantic loss score replicates previous findings based on classifier performance. Finally, using this score, we demonstrate that compression-based measures outperform state-of-the-art vector-embedding-based approaches, such as CodeBERT and GraphCodeBERT, on unformatted code, but lag behind when the code is formatted or compiled and then decompiled. This indicates that these approaches are sensitive to the varying formatting of code.

ABSTRACT. Software development is a process of gradually modifying program behavior; thus, most programs are revisions of other programs. Developers informally reason about a revision in terms of which behaviors are removed, added, or preserved. We formalize these notions by providing a collecting semantics for program revisions, parameterized by a user-specified state correspondence, which classifies reachable states as ``removed'', ``added'', or ``related''. Intuitively, reasoning about added and removed states requires showing that some reachable state in one program has no corresponding state in the other. Therefore, proving safety properties over removed and added states requires an underapproximation of one program and an overapproximation of the other. Existing relational Hoare-style program logics provide limited support for reasoning about this class of properties. To address this gap, we present a system for proving safety properties of ``added'', ``removed'', and ``related'' states that combines over- and underapproximating program logics.

ABSTRACT. We flesh out that *equivalence checking* constitutes a form of backward-complete *abstract interpretation* on pairs of programs. The first part of the paper illustrates this framing for trace semantics on finite-state systems. We then extend the approach to uniformly handle simulation, failure equivalence, and ready simulation in a single abstract interpretation.

ABSTRACT. Hyperproperties relate multiple executions of a program and capture essential correctness and security properties such as determinism, monotonicity, transitivity, reachability, and (generalized) non-interference. Existing program logics for hyperproperties typically reason about a fixed number of states, which limits the kinds of hyperproperties they can express and prove, and hinders the reuse of proofs across different formalisms. In this talk, I will present Hyper Hoare Logic (HHL), a generalization of Hoare logic whose assertions range over sets of states rather than individual states. This generalization enables uniform reasoning for a wide range of hyperproperties, including those beyond the reach of existing logics. Despite its expressiveness, HHL admits simple and intuitive inference rules that support key reasoning principles, such as composing different kinds of hyperproperties in the same proof or reasoning about loops where different executions perform different numbers of iterations. I will then show that HHL lends itself to automation through Hypra, an automated verifier that translates a program and its HHL specification into a Viper program, with each Viper execution representing a set of executions of the original program. Our evaluation on new and existing benchmarks shows that Hypra can automatically prove diverse hyperproperties efficiently and with minimal annotation overhead. Finally, I will turn to Hyper Separation Logic, a recent extension of HHL that brings modular reasoning about hyperproperties to heap-manipulating programs. Its key ingredient is a hyper separating conjunction that lifts the standard separating conjunction to sets of states, yielding a generalized frame rule for hyperproperties.

ABSTRACT. In this project, we explored Dafny's capabilities in proving program equivalence. We built EquiDafny, an equivalence checker on top of Dafny to generate equivalence proofs automatically, with no user assistance. Finally, we evaluated EquiDafny against program verifiers Dafny and Stainless.

ABSTRACT. We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a sound and complete certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1)~it is fully automated, (2)~it is applicable to infinite-state probabilistic programs, and (3)~it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.

ABSTRACT. Although techniques for the verification of neural networks (NNs) have seen significant progress in recent years, specifying meaningful properties remains non-trivial. One promising approach to the specification of neural networks are relational properties which do not specify the behavior of an NN in absolute terms, but impose constraints on related execution traces. We provide an overview of our recent advances in using differential verification in NN verification by leveraging the abstract domain of Zonotopes. This approach enables us to reason about changes in behavior locally, at the level of individual neurons of an NN. We discuss the fundamental ideas of our abstract domain and discuss current and future applications of the differential verification paradigm.