« earlier | later » Page 1 of 1

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

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

« earlier | later » Page 1 of 1

- formal-methods | |

1 | + browser |

1 | + compiler |

1 | + concurrency |

1 | + correctness |

1 | + cryptography |

1 | + java |

1 | + language-design |

1 | + memory |

1 | + occam |

1 | + openssl |

1 | + publications |

1 | + python |

1 | + reference |

2 | + research |

1 | + rust |

1 | + scheme |

3 | + security |

1 | + separation-logic |

1 | + sorting |

1 | + ssl |

1 | + tls |

3 | + verification |

1 | + web |

tasty by Adam Sampson.