Tim Peters developed the Timsort hybrid sorting algorithm in 2002. It is a clever combination of ideas from merge sort and insertion sort, and designed to perform well on real world data. TimSort was first developed for Python, but later ported to Java(where it appears as java.util.Collections.sort and java.util.Arrays.sort) by Joshua Bloch(the designer of Java Collections who also pointed out that most binary search algorithms were broken). TimSort is today used as the default sorting algorithm for Android SDK, Sun’s JDK and OpenJDK. Given the popularity of these platforms this means that the number of computers, cloud services and mobile phones that use TimSort for sorting is well into the billions.
Fast forward to 2015. After we had successfully verified Counting and Radix sort implementations in Java(J. Autom. Reasoning 53(2), 129-139) with a formal verification tool called KeY, we were looking for a new challenge. TimSort seemed to fit the bill, as it is rather complex and widely used. Unfortunately, we weren’t able to prove its correctness. A closer analysis showed that this was, quite simply, because TimSort was broken and our theoretical considerations finally led us to a path towards finding the bug(interestingly, that bug appears already in the Python implementation). This blog post shows how we did it.
CERT is the world’s leading trusted authority dedicated to improving the security and resilience of computer systems and networks. A reference in secure-coding:
Writing secure C code helps you avoid the software defects most likely to cause exploitable vulnerabilities. SEI CERT C Coding Standard: Rules for Developing Safe, Reliable, and Secure Systems(2016 Edition) identifies the root causes of today's most widespread software vulnerabilities, shows how they can be exploited, reviews the potential consequences, and presents secure alternatives. This online download is available for free to promote the adoption of secure coding standards for C and C++.
What Can Agile Methods Bring to High-Integrity Software Development?
Joint paper from ProteanCode and Altran UK on how Agile approaches can be used, improved and deployed in the development of high-integrity software.
Formal Verification of Adventure Games using CBMC
The Teeny Tiny Mansion(TTTM) is a mockup text adventure game that is formally proven to have no"dead ends". I.e. all player actions will result in a state in which the game is still winnable.
Computer scientists can prove certain programs to be error-free with the same certainty that mathematicians prove theorems. The advances are being used to secure everything from unmanned drones to the internet.
Moving Fast with Software Verification at Facebook
For organisations like Facebook, high quality software is important. However, the pace of change and increasing complexity of modern code makes it difficult to produce error free software. Available tools are often lacking in helping programmers develop more reliable and secure applications.
Formal verification is a technique able to detect software errors statically, before a product is actually shipped. Although this aspect makes this technology very appealing in principle, in practice there have been many difficulties that have hindered the application of software verification in industrial environments. In particular, in an organisation like Facebook where the release cycle is fast compared to more traditional industries, the deployment of formal techniques is highly challenging.
Proving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it)
The CERT Division of the Software Engineering Institute at Carnegie Mellon University
What Can Agile Methods Bring to High-Integrity Software Development?
Formal Verification of Adventure Games using CBMC
Hacker-Proof Code Confirmed
Moving Fast with Software Verification at Facebook