The slides can be downloaded here. Abstract: The UTxO (unspent transaction output) model is the underlying data structure of Bitcoin, which has since been extended to the Extended UTxO model. It exists in code, but what does it mean?  I will give a novel mathematical model based on some strikingly simple type equations which — for […]

Abstract: The rise of machine learning (ML) and artificial intelligence (AI) have instigated significant interests in developing domain specific integrated circuits and architectures that can support the computational demands of AI. These chips are commonly known as AI chips. AI chips, both for training and inferencing, have emerged out to be new areas of research and […]

This tech talk has been canceled and will be rescheduled. We apologize for the inconvenience! Abstract: Computational science uses a computer’s super power and mathematical algorithms to solve large-scale scientific problems. Data science explores information from large quantity heterogeneous datasets to gain insights and build forecast models with statistical methods. Wouldn’t it be great to […]

This tech talk has been canceled and will be rescheduled. We apologize for the inconvenience! This talk will be live-streamed at: https://www.youtube.com/c/GaloisInc/live Abstract: “My programs just write themselves!”  This phrase is frequently exclaimed by users of functional programming languages with advanced type systems who observe that rich types often guide them directly towards correct programs.  […]

Abstract: Many software systems employ parsing techniques to map sequential input to structured output. Often, a parser is the system component that consumes data from an untrusted source. Because parsers mediate between the outside world and application internals, they are good targets for formal verification; parsers that come with strong correctness guarantees are likely to […]

Abstract:Formal verification has become a well-established part of standard hardware design flows leveraging SAT solvers and model checkers for verification tasks including logical equivalence checking, property checking, and protocol verification. These tools are largely based on all-digital, synchronous, single clock-domain models of hardware behaviour. To address the needs of system-on-chip and multi-core designs, we are […]

Abstract:My talk will present a distributed secure architecture for “cellularization,” a process in which utilities of the players are aligned by credible/non-credible threats. The proposed solution relies on a novel decentralized permissionless cyber-physical architecture that enables players to participate in Information-Asymmetric (Signaling) games, where deception is tamed by costly signaling, formal verification and zero-knowledge cryptography. […]

Abstract: Developing interactive apps against event-driven software frameworks, like Android, is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that can then in turn […]

Abstract The study of quantum computation has been motivated, in part, by the possibility that quantum computers can perform certain tasks dramatically faster than classical computers. Many of the known quantum-over-classical speedups, such as Shor’s algorithm for factoring integers and Grover’s search algorithm, can be framed as oracle problems or concept learning problems. In one […]

Abstract:  This talk will present some of the basic principles of chip design including an overview of how chips are manufactured. Then I will give an overview of the complexity of chip design by focusing on addition. While it may seem like a basic operation, people have spent careers optimizing arithmetic circuits like adders. I […]