Tasty » Adam Sampson's verification bookmarks

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

Language-theoretic Security edit / delete

"The Language-theoretic approach (LANGSEC) regards the Internet insecurity epidemic as a consequence of ad hoc programming of input handling at all layers of network stacks, and in other kinds of software stacks." Some interesting work, although it's obviously focussing on one class of problem...

to langsec language-design parser proof security verification ... on 03 January 2015

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