Tasty » Adam Sampson's correctness bookmarks

European Spreadsheet Risks Interest Group - spreadsheet risk management and solutions conference edit / delete

I like this idea.

to correctness risks spreadsheet ... on 29 June 2020

Finding bugs in Haskell code by proving it – Blog – Joachim Breitner's Homepage edit / delete

A worked example of using hs-to-coq.

to coq correctness formal-verification functional haskell ... on 10 December 2017

A Guide to Undefined Behavior in C and C++, Part 1 – Embedded in Academia edit / delete

A good overview for students.

to c cmp201 correctness language-design safety teaching undefined-behaviour ... on 10 February 2017

Let’s stop copying C / fuzzy notepad edit / delete

Yes, let's. Please.

to amusements c correctness language-design safety ... on 10 February 2017

Software Foundations edit / delete

Practical proof in programming; based on Coq. Full text of the book available online.

to coq correctness proof teaching ... on 10 February 2017

Notes on concurrency bugs edit / delete

A couple of studies (now a few years old) looking at what kinds of concurrency bugs show up in real software.

to concurrency correctness debugging software-engineering ... on 28 August 2016

Files are hard edit / delete

A comprehensive study of what might go wrong when trying to guarantee that data has been written to disk.

to correctness email fs os ... on 31 December 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

Embedded in Academia : Compilers and Termination Revisited edit / delete

A surprising example of C++ optimisation -- optimising out a loop with no side effects other than non-termination.

to c++ compiler correctness optimisation ... on 01 April 2014