wrhn

Recent submissions

Comment · 9 years ago
Design verification using TLA+ and Alloy is a completely different game than verification at the level of code as in Verdi. While there are plenty of studies saying design verification is good in general, I'm not aware of any studies saying that (or quantifying to what degree) it gets you close to implementation verification. On the flip side, the classic paper on the implementation of Paxos hints at just at how wide the gap is between design and running systems: https://research.google.com/archive/paxos_made_live.html

While Frama-C style verification works well out-of-the-box for proving single-threaded, isolated programs correct, one has to make a major effort to capture assumption-heavy distributed systems behavior using ghost code and other tricks. The only effort I'm aware of in this direction is the following, which uses the VCC tool: http://madhu.cs.illinois.edu/evcons.pdf

Comment · 9 years ago
If you're looking for programs verified down to the machine code level, using C and the Verified Software Toolchain (VST) is one option. C programs are proven in the Hoare style (pre/postconditions) inside Coq, and then compiled using the verified CompCert compiler. Properties proven in Coq are guaranteed to hold about the compiled code.

There is nothing fundamental to prevent using VST to prove Verdi handler code correct, but the current runtime is not set up for that workflow.

http://vst.cs.princeton.edu

Comment · 9 years ago
Some new developments of the framework in the last two years:

- packaging via OPAM to separate framework code and system code

- support for specifying and proving liveness properties

- support for proving Abadi/Lamport style refinement mappings between systems

The following workshop paper gives an overview of current and upcoming work: http://conf.researchr.org/event/CoqPL-2017/main-verification...

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton