Abstract: We will give a general introduction to Gillian, a platform for the development of symbolic-execution tools for many programming languages.  Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations […]

Abstract: Advances in deep neural networks (DNNs) have increased their deployment in safety-critical systems, such as vision perception modules for autonomous vehicles and airborne collision avoidance system controllers for unmanned aircraft. Modern DNNs and linear classifiers are susceptible to adversarial input perturbations. Adversarial perturbations are small changes to an input that result in unexpected changes […]

The slides for this presentation can be found here. Abstract: Porting operating systems is expensive; it costs time and money and (particularly) the attention of senior developers. Furthermore, with the end of Moore’s Law, portability is becoming more important again. Against this background, recent advances in program synthesis and the increasing availability of formal specifications for machine architectures offer an […]

Abstract: Secure multi-party computation (MPC) allows multiple parties, each holding private data that they are unwilling to share, to collaborate to perform computations over their data, while revealing nothing other than the result.  The theory behind secure computation is already 35 years old, but in the last 15 years researchers in the field have demonstrated […]

The slides can be downloaded here. Abstract: In the real world, people join humanity, grow up trusting very different quorums from one another, and they may change their quorums with time.  In technical terms we could call this an open permissionless system with mutable local quorums.   One might expect such a system to be a […]

Abstract: Increasing set of functionalities, network interoperability, and system design complexity have introduced easily exploitable security vulnerabilities in cyber-physical systems (CPS). Furthermore, the tight interaction between information technology and physical world, as well as the rising levels of autonomy, make these systems vulnerable to attacks beyond the standard cyber-attacks; relying exclusively on conventional security techniques […]

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.  […]