We consider the problem of entity alignment in multi-modal knowledge graphs (MMKGs). The explosion in interest in MMKGs has led to a wide array of techniques used to align entities within multiple MMKG’s. The nature of the different modalities available in the MMKG makes the act of embedding them in a shared space challenging. This paper proposes using optimal transport (OT) as a means of embedding and aligning multiple modalities into one unified representation [1]. After acquiring the unified representation, we propose using contrastive learning to train a model for better performance in accurately predicting links between entities. Experiments looking at the effect of the additional modality and OT data fusion show poor performance failed to meet, let alone exceed, current state of the art.

Linear type systems are powerful because they can statically ensure the correct management of resources like memory, but they can also be cumbersome to work with, since even benign uses of a resource require that it be explicitly threaded through during computation. Borrowing , as popularized by Rust, reduces this burden by allowing one to temporarily disable certain resource permissions (e.g., deallocation or mutation) in exchange for enabling certain structural permissions (e.g., weakening or contraction). In particular, this mechanism spares the borrower of a resource from having to explicitly return it to the lender but nevertheless ensures that the lender eventually reclaims ownership of the resource. In this paper, we elucidate the semantics of borrowing by starting with a standard linear type system for ensuring safe manual memory management in an untyped lambda calculus and gradually augmenting it with immutable borrows, lexical lifetimes, reborrowing, and finally mutable borrows. We prove semantic type soundness for our Borrow Calculus ( BoCa ) using Borrow Logic ( BoLo ), a novel domain-specific separation logic for borrowing. We establish the soundness of this logic using a semantic model that additionally guarantees that our calculus is terminating and free of memory leaks. We also show that our Borrow Logic is robust enough to establish the semantic safety of some syntactically ill-typed programs that temporarily break but reestablish invariants.

This paper presents the design of Forge , a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry. Forge offers a progression of languages that improve the learning experience by only gradually increasing in expressive power. Forge supports custom visualization of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of testing features to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use.

The Application Binary Interface (ABI) for a language defines the interoperability rules for its target platforms, including data layout and calling conventions, such that compliance with the rules ensures “safe” execution and perhaps certain resource usage guarantees. These rules are relied upon by compilers, libraries, and foreign- function interfaces. Unfortunately, ABIs are typically specified in prose, and while type systems for source languages have evolved, ABIs have comparatively stalled, lacking advancements in expressivity and safety. We propose a vision for richer, semantic ABIs to improve interoperability and library integration, supported by a methodology for formally specifying ABIs using realizability models. These semantic ABIs connect abstract, high-level types to unwieldy, but well-behaved, low-level code. We illustrate our approach with a case study formalizing the ABI of a functional source language in terms of a reference-counting implementation in a C-like target language. A key contribution supporting this case study is a graph-based model of separation logic that captures the ownership and accessibility of reference-counted resources using modalities inspired by hybrid logic. To highlight the flexibility of our methodology, we show how various design decisions can be interpreted into the semantic ABI. Finally, we provide the first formalization of library evolution, a distinguishing feature of Swift’s ABI.

Compared to ordinary concurrent and distributed systems, cryptographic protocols are distinguished by the need to reason about interference by adversaries. We suggest a new layered approach to tame that complexity, via an executable protocol language whose semantics does not reveal an adversary directly, instead enforcing a set of intuitive hygiene rules. By virtue of those rules, protocols written in this language provably behave identically with or without interference by active Dolev-Yao-style adversaries. As a result, formal reasoning about protocols can be simplified enough that even naïve model checking can establish correctness of a multiparty protocol, through analysis of a state space with no adversary. We present the design and implementation of SPICY, short for Secure Protocols Implemented CorrectlY, including the semantics of its input languages; the essential safety proofs, formalized in the Coq theorem prover; and the automation techniques. We provide a preliminary evaluation of the tool's performance and capabilities via a handful of case studies.

Programs are rarely implemented in a single language, and thus questions of type soundness should address not only the semantics of a single language, but how it interacts with others. Even between type-safe languages, disparate features can frustrate interoperability, as invariants from one language can easily be violated in the other. In their seminal 2007 paper, Matthews and Findler proposed a multi-language construction that augments the interoperating languages with a pair of boundaries that allow code from one language to be embedded in the other. While this technique has been widely applied, their syntactic source-level interoperability doesn’t reflect practical implementations, where the behavior of interaction is only defined after compilation to a common target, and any safety must be ensured by target invariants or inserted target-level “glue code.”

Configuring a service mesh often involves multiple parties, each of whom is responsible for separate portions of the overall system. This can result in miscommunication, silent and sudden errors, or a failure to meet goals.

Many classic and contemporary face recognition algorithms work well on public data sets, but degrade sharply when they are used in a real recognition system. This is mostly due to the difficulty of simultaneously handling variations in illumination, image misalignment, and occlusion in the test image. We consider a scenario where the training images are well controlled and test images are only loosely controlled. We propose a conceptually simple face recognition system that achieves a high degree of robustness and stability to illumination variation, image misalignment, and partial occlusion. The system uses tools from sparse representation to align a test face image to a set of frontal training images. The region of attraction of our alignment algorithm is computed empirically for public face data sets such as Multi-PIE. We demonstrate how to capture a set of training images with enough illumination variation that they span test images taken under uncontrolled illumination. In order to evaluate how our algorithms work under practical testing conditions, we have implemented a complete face recognition system, including a projector-based training acquisition system. Our system can efficiently and effectively recognize faces under a variety of realistic conditions, using only frontal images under the proposed illuminations as training.

Most contemporary face recognition algorithms work well under laboratory conditions but degrade when tested in less-controlled environments. This is mostly due to the difficulty of simultaneously handling variations in illumination, alignment, pose, and occlusion. In this paper, we propose a simple and practical face recognition system that achieves a high degree of robustness and stability to all these variations. We demonstrate how to use tools from sparse representation to align a test face image with a set of frontal training images in the presence of significant registration error and occlusion. We thoroughly characterize the region of attraction for our alignment algorithm on public face datasets such as Multi-PIE. We further study how to obtain a sufficient set of training illuminations for linearly interpolating practical lighting conditions. We have implemented a complete face recognition system, including a projector-based training acquisition system, in order to evaluate how our algorithms work under practical testing conditions. We show that our system can efficiently and effectively recognize faces under a variety of realistic conditions, using only frontal images under the proposed illuminations as training.

Partially occluded faces are common in many applications of face recognition. While algorithms based on sparse representation have demonstrated promising results, they achieve their best performance on occlusions that are not spatially correlated (i.e. random pixel corruption). We show that such sparsity-based algorithms can be significantly improved by harnessing prior knowledge about the pixel error distribution. We show how a Markov Random Field model for spatial continuity of the occlusion can be integrated into the computation of a sparse representation of the test image with respect to the training images. Our algorithm efficiently and reliably identifies the corrupted regions and excludes them from the sparse representation. Extensive experiments on both laboratory and real-world datasets show that our algorithm tolerates much larger fractions and varieties of occlusion than current state-of-the-art algorithms.

This work builds on the method of [6] to create a prototype access control system, capable of handling variations in illumination and expression, as well as significant occlusion or disguise. Our demonstration will allow participants to interact with the algorithm, gaining a better understanding strengths and limitations of sparse representation as a tool for robust recognition.

We consider the problem of simultaneously segmenting data samples drawn from multiple linear subspaces and estimating model parameters for those subspaces. This "subspace segmentation" problem naturally arises in many computer vision applications such as motion and video segmentation, and in the recognition of human faces, textures, and range data. Generalized Principal Component Analysis (GPCA) has provided an effective way to resolve the strong coupling between data segmentation and model estimation inherent in subspace segmentation. Essentially, GPCA works by first finding a global algebraic representation of the unsegmented data set, and then decomposing the model into irreducible components, each corresponding to exactly one subspace. We provide a summary of important algebraic properties and statistical facts that are crucial for making GPCA both efficient and robust, even when the given data are corrupted with noise or contaminated by outliers. We demonstrate the effectiveness of GPCA using a large testbed of synthetic and real experiments.

Reconstruction of the point source of blood splatter in a crime scene is an important and difficult problem in forensic science. We study the problem of automatically reconstructing the 3-D location of the victim of a shooting from photographs of planar surfaces with blood splattered on them. We analyze this problem in terms of the multiple-view geometry of planar conic sections. Using projective invariants associated with pairs of conic sections, we match images of multiple conic sections taken from widely separated viewpoints. We further recover the homography between two views using the common tangents of pairs of conic sections. The location of the point source is then retrieved from the reconstructed scene geometry. We suggest how to extend these results to scenes containing multiple planar surfaces, and verify the proposed method with experiments on both synthetic and real images.

We study and compare two novel embedding methods for segmenting feature points of piece-wise planar structures from two (uncalibrated) perspective images. We show that a set of different homographies can be embedded in different ways to a higher-dimensional real or complex space, so that each homography corresponds to either a complex bilinear form or a real quadratic form. Each embedding reveals different algebraic properties and relations of homographies. We give a closed-form segmentation solution for each case by utilizing these properties based on subspace-segmentation methods. These theoretical results show that one can intrinsically segment a piece-wise planar scene from 2-D images without explicitly performing any 3-D reconstruction. The resulting segmentation may make subsequent 3-D reconstruction much better-conditioned. We demonstrate the proposed methods with some convincing experimental results.

In this paper, we investigate the mathematical problem underlying segmentation of hybrid motions: given a series of tracked feature correspondences between two (perspective) images, we seek to segment and estimate multiple motions, possibly of different types (e.g., affine, epipolar, and homography). In order to accomplish this task, we cast the problem into a more general mathematical framework of segmenting data samples drawn from a mixture of linear subspaces and quadratic surfaces. The result is a novel algorithm called hybrid quadratic surface analysis (HQSA). HQSA uses both the derivatives and Hessians of fitting polynomials for the data to separate linear data samples from quadratic data samples. These derivatives and Hessians also lead to important necessary conditions, based on the so-called mutual contraction subspace, to separate data samples on different quadratic surfaces. The algebraic solution we derive is non-iterative and numerically stable. It tolerates moderate noise and can be used in conjunction with outlier removal techniques. We show how to solve the hybrid motion segmentation problem using HQSA, and demonstrate its performance on simulated data with noise and on real perspective images.