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

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

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

Abstract:  Teaching programming is a hard job. Teaching Haskell is a way harder given its inherent complexity and expectations students have. Nevertheless, there are many approaches to do that. In this talk, I would like to outline the practices that I use and those that I don’t find fruitful. There are quite a few books […]

Title: Formally Verifying Implementations of Distributed Systems Abstract: Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. In this talk, we’ll survey the Verdi […]

Abstract: Lean is an interactive theorem prover and functional programming language. Lean implements a version of the Calculus of Inductive Constructions. Its elaborator and unification algorithms are designed around the use of type classes, which support algebraic reasoning, programming abstractions, and other generally useful means of expression. Lean has parallel compilation and checking of proofs, […]

Abstract: In this talk, I’ll give a high-level overview of Penn’s Vellvm (Verified LLVM) project, which aims to build formal semantics in Coq for the LLVM IR. I’ll sketch some of our past results, in which we verified memory safety transformations and a variant of LLVM’s mem2reg optimization, focusing on the structure of the proof techniques.  Along the way, […]

Abstract: Verification is often the dominant cost in the design of critical systems. In this talk, we advocate the use of refinement to reason about critical systems. The idea is that a system is correct if all of its observable behaviors are allowed by an abstract system that acts as the specification. For example, to […]

Abstract: It has been said that Documentation/memory-barriers.txt can be used to frighten small children [1], and perhaps this is true. However, it is woefully inefficient.  After all, there are a very large number of children in this world, and it would take a huge amount of time and effort to read it to all of them. This situation clearly […]

Abstract: In this talk we present a systematic effort that can automatically repair firewalls, using the programming by example approach. Firewalls are widely employed to manage and control enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of policies, ensuring the correctness of firewalls – whether the policies in the firewalls meet the specifications of […]