Document and protocol formats are the languages in which computing systems exchange information. The notion of a “document-format” certainly isn’t foreign to most computer users: everyday, vast swaths of users directly create, edit, and share documents and media in formats such as PDF, JPEG, and Word. But in principle, the concept of a “format” is […]
At Galois, we develop formal verification tools that rely on a variety of automated solvers for answering mathematical queries. The main solvers we use are called Satisfiability Modulo Theories (SMT) solvers. These solvers offer the ability to answer questions such as “find me inputs for which a mathematical property holds.” We have found these tools […]
I’m excited to announce we’ve been awarded a $7.5 million contract by the Defense Advanced Research Projects Agency (DARPA) to work on PIRATE, a set of software development tools for designing and building high-performance, physically-partitioned applications that protect sensitive information. PIRATE stands for Partitioning Information via Resource-Aware Transformations for Everyone. The project is part of […]
Secure computation enables users to compute some result without revealing the inputs. Privacy schemes that are shown to only reveal outputs are said to have input privacy. However, learning these outputs still tells you something about the private inputs. The important question is: “how much?” The Defense Advanced Research Projects Agency (DARPA) Brandeis program aims […]
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 […]
Projections based on data models for COVID-19 are serving as a critical foundation for Federal, state and local government policy makers charged with making rapid and informed decisions to fight the spread of the novel coronavirus. Data models like the model presented by researchers at Imperial College London on March 16, which many believe led […]
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. […]
2019 marked another eventful year for Galois, publishing 15 papers, sharing 26 talks, and announcing several large project awards. It seems cliche, but it’s true: our partners and collaborators play a central role in all of our work. We’re very grateful to be part of such a great community. Below, we highlight some of the […]
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.