TLA+ model checking made symbolic

November 29, 2019May 25, 2020 ~ Adrian Colyer ~ 10 Comments

TLA+ model checking made symbolic Konnov et al., OOPSLA'19 TLA+ is a formal specification language (Temporal Logic of Actions) particularly well suited to reasoning about distributed algorithms. In addition to the specification language, the TLA+ toolset includes a model checker (TLC) and a theorem prover (TLAPS). Given the huge state spaces involved in many real-world ... Continue Reading

Formal foundations of serverless computing

November 18, 2019May 25, 2020 ~ Adrian Colyer ~ 2 Comments

Formal foundations of serverless computing Jangda et al., OOPSLA'19 Jangda et al. won a distinguished paper award at OOPSLA this year for their work on ‘Formal foundations of serverless computing.’ Central to the paper is their observation that the serverless execution environment has a number of unique properties (such as warm starting / reuse of ... Continue Reading

Scaling symbolic evaluation for automated verification of systems code with Serval

November 13, 2019May 25, 2020 ~ Adrian Colyer ~ 2 Comments

Scaling symbolic evaluation for automated verification of systems code with Serval Nelson et al., SOSP'19 Serval is a framework for developing automated verifiers of systems software. It makes an interesting juxtaposition to the approach Google took with Snap that we looked at last time out. I’m sure that Google engineers do indeed take extreme care ... Continue Reading

Learning to prove theorems via interacting with proof assistants

August 23, 2019May 25, 2020 ~ Adrian Colyer ~ 13 Comments

Learning to prove theorems via interacting with proof assistants Yang & Deng, ICML'19 Something a little different to end the week: deep learning meets theorem proving! It’s been a while since we gave formal methods some love on The Morning Paper, and this paper piqued my interest. You’ve probably heard of Coq, a proof management ... Continue Reading

Programming and proving with distributed protocols

January 22, 2018 ~ Adrian Colyer ~ Leave a comment

Programming and proving with distributed protocols Sergey et al., POPL 18 Last week we looked at the verification of Rust’s type-based safety guarantees, and a verification toolchain for proving properties of JavaScript programs. Today it’s the turn of Disel, a framework for developing and verifying message-passing based distributed systems (it would seem to fit beautifully ... Continue Reading

JaVerT: JavaScript Verification Toolchain

January 19, 2018 ~ Adrian Colyer ~ 4 Comments

JaVerT: JavaScript Verification Toolchain Santos et al., POPL 18 The JavaScript Verification Toolchain (JaVerT) is designed to support reasoning over JavaScript programs. It can be used to verify functional correctness properties of programs annotated with pre- and post- conditions, loop invariants, and instructions for unfolding and folding user-defined predicates. To do this, it must be ... Continue Reading

A model for reasoning about JavaScript promises

November 10, 2017 ~ Adrian Colyer ~ 1 Comment

A model for reasoning about JavaScript promises§ Madsen et al., OOPSLA’17 As an antidote to callback-hell, ECMAScript 6 introduces Promises. Promises represent the value of an asynchronous computation, and the functions resolve and reject are used to settle the promise. Promises can be chained using then. However, the semantics of JavaScript promises are quite complex, ... Continue Reading

HoTTSQL: Proving query rewrites with univalent SQL semantics

October 5, 2017 ~ Adrian Colyer ~ Leave a comment

HoTTSQL: Proving query rewrites with univalent SQL semantics Chu et al., PLDI’17 Query rewriting is a vital part of SQL query optimisation, in which rewrite rules are applied to a query to transform it into forms with (hopefully!) a lower execution cost. Clearly when a query is rewritten we still want it to mean the ... Continue Reading

Growing a protocol

August 23, 2017 ~ Adrian Colyer ~ Leave a comment

Growing a protocol Ramasubramanian et al., HotCloud'17 I've been really enjoying working my way through a selection of the HotCloud papers - they're relatively short, thought-provoking, and designed to promote discussion (each paper has a set of discussion questions at the very end - great if you're looking at them in a group of some ... Continue Reading

An empirical study on the correctness of formally verified distributed systems

May 29, 2017 ~ Adrian Colyer ~ 9 Comments

An empirical study on the correctness of formally verified distributed systems Fonseca et al., EuroSys'17 "Is your distributed system bug free?" "I formally verified it!" "Yes, but is your distributed system bug free?" There's a really important discussion running through this paper - what does it take to write bug-free systems software? I have a ... Continue Reading

the morning paper

a random walk through Computer Science research, by Adrian Colyer
Made delightfully fast by strattic

Formal methods