Semantic Foundations for Live Programming Environments

Monday, April 08, 2019

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

Wednesday, March 27, 2019

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

Wednesday, December 19, 2018

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

Tuesday, December 18, 2018

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

Teaching Haskell in the Real World

Friday, December 14, 2018

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

Read More

Public Tech Talk: Formally Verifying Implementations of Distributed Systems

Thursday, September 13, 2018

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

Read More

The Lean Theorem Prover: Past, Present and Future

Friday, August 03, 2018

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

Read More

Vellvm – Verifying the LLVM

Friday, July 13, 2018

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

Read More

Canceled: Reasoning about Critical Systems using Refinement

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

Read More

Linux-Kernel Memory Ordering: Help Arrives At Last!

Wednesday, May 16, 2018

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

Read More