Tasty » Adam Sampson's formal-methods bookmarks

Formal validation of the Arm v8-M specification – Alastair Reid – Researcher at ARM Ltd edit / delete

Alastair gave a presentation about this at a workshop I attended; very interesting stuff (and his blog generally is well worth reading).

to arm ers formal-methods security validation ... on 05 May 2018

Kryptos Logic Research: OpenSSL's squaring bug, and opportunistic formal verification edit / delete

Detecting an OpenSSL bug (after the fact) using formal verification. Interesting because the original formal proof was wrong...

to formal-methods openssl security ssl ... on 16 March 2015

Proving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it) | Envisage: Engineering Virtualized Services edit / delete

Using formal methods to find a pretty serious bug.

to correctness formal-methods java python sorting verification ... on 14 March 2015

Reasoning About the Heap in Rust edit / delete

Quote: "it's still worth applying Separation logic to get a feel for what's happening to the heap". I'm kind of impressed that the Rust designers have managed to come up with a design for reference types that's *more* complex than C++'s.

to formal-methods language-design memory reference rust separation-logic ... on 03 May 2014

miTLS - Home edit / delete

A formally verified implementation of TLS. (Being written in F# means it's a bit impractical to use as a library, though...)

to cryptography formal-methods security tls verification ... on 28 April 2014

Quark : A Web Browser with a Formally Verified Kernel edit / delete

Building a formally-verified sandbox for browser components. Neat!

to browser formal-methods security verification web ... on 12 November 2013

Bill Roscoe - Home Page edit / delete

to concurrency formal-methods occam publications ... on 08 May 2010

ACL2 in DrScheme edit / delete

A theorem prover.

to formal-methods research scheme ... on 11 March 2006

The Compcert certified compiler back-end edit / delete

A compiler that has been proved correct (in CoQ).

to compiler formal-methods research ... on 04 February 2006