Public Tech Talk: A Verified LL(1) Parser Generator

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

Read More

Public Tech Talk – Formal Hardware Verification: Asynchronous, Analog, Mixed-Signal, and Mixed-Timing Circuits

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

Read More

Public Tech Talk – Cellularization: A Game Theoretic Perspective

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

Read More

Fixr: Mining and Understanding Bug Fixes for App-Framework Protocol Defects

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

Read More

Quantum Learning from Symmetric Oracles

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

Read More

Semantic Foundations for Live Programming Environments

Abstract: When programming, it is common to spend minutes, hours, or even days at a time working with program text where there are missing pieces, type errors, or merge conflicts. Programming environments have trouble generating meaningful feedback in these situations because programming language definitions typically assign formal meaning only to fully-formed, well-typed programs. Lacking timely and […]

Read More

Goldilocks the Verification Engineer

Abstract: In this talk, I will describe three approaches to verifying distributed systems using inductive invariants: manual proof, automated proof, and invariant inference. These techniques offer increasing levels of automation, but at some cost. I will argue that the middle technique strikes a good balance for users, and that it is possible for a tool to be […]

Read More

Toward Assured and Resilient Autonomous Systems Operations

Abstract:  Cyber-physical systems (CPS) and especially autonomous vehicles like drones and driverless cars are becoming increasingly popular thanks to their sophisticated hardware and software capabilities. As they find their way into our society, it becomes imperative to guarantee that they can always be safe even during unforeseen and unpredictable events. Unfortunately, at the moment there […]

Read More

Runtime Monitors for Hybrid Mobile Apps and Other Stories

Abstract: The formidable growth of the cyber-threat landscape today is accompanied by an imperative need for providing high-assurance software solutions. In the last decade, binary hardening via In-lined Reference Monitoring (IRMs) has been firmly established as a powerful and versatile technology, providing superior security enforcement for many platforms. IRM frameworks rewrite untrusted binary code, inserting […]

Read More