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
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
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
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
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
Friday, February 02, 2018
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 […]
Read More
Monday, January 15, 2018
Abstract: The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. In this talk, I will describe JaVerT, a semi-automatic JavaScript Verification Toolchain based on separation logic. JaVerT is aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. The specification challenge is to […]
Read More
Tuesday, December 19, 2017
Abstract: Developer tools that support multiple languages generally have very limited regex-based code-analysis capabilities. Tree-sitter is a new parsing system that aims to change this paradigm. We’re in the process of integrating Tree-sitter into both GitHub.com and Atom, which will allow us to analyze code accurately and in real-time, paving the way for better syntax […]
Read More
Friday, December 08, 2017
Abstract: Habit is a high-level programming language, originally based on Haskell, that was designed to meet the needs of high assurance, very low-level software development. The most recent version of the language report was completed in 2010, and an initial working prototype implementation was developed by the HASP group at PSU. However, there has not […]
Read More
Monday, October 23, 2017
Abstract: Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power […]
Read More