Export or edit this venue...

Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)

Future events happening here

  • - No events -

Past events that happened here

  • Thursday
    Sep 13 2018
    Public Tech Talk: Formally Verifying Implementations of Distributed Systems


    Formally Verifying Implementations of Distributed Systems


    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 project which provides a framework for implementing and formally verifying implementations of distributed systems in Coq. Verdi eases the verification burden by enabling developers to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. Using this approach, the Verdi team produced the first correctness proof for an implementation of the Raft distributed consensus protocol.


    Zach Tatlock is an Assistant Professor in Computer Science and Engineering at the University of Washington where he leads the Programming Languages and Software Engineering (PLSE) group. He received his PhD from UC San Diego and BS from Purdue (where he took nearly every course with Bill Harris!). His research draws upon proof assistants, SMT solvers, and type systems to improve software reliability and security in domains ranging from distributed systems and compilers to web browsers. He can juggle and solve Rubik’s cubes, but not at the same time.

  • Tuesday
    Dec 19 2017
    Galois Tech Talk: Tree-Sitter: A New Parsing System for Programming Tools

    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 highlighting, code navigation, and refactoring support. We’ll demo some new features that Tree-sitter has enabled in GitHub.com and Atom, discuss its implementation, and share thoughts on ways it could be used in the future.

    Bio: Max Brunsfeld is an engineer on GitHub’s Atom team. Prior to joining GitHub, he worked at Pivotal Labs as a full-stack engineer. He enjoys programming, especially in C and C++, jazz guitar, bicycling and hiking. He lives in Portland with his wife and two toddlers.