In July 2015 ERCIM News No. 102 was published at http://ercim-news.ercim.eu/en102
Special Theme: "Trustworthy Systems of Systems"
Guest editors: Poul Heegaard, NTNU and Erwin Schoitsch, Austrian Institute of Technology
From the Netherlands, there are contributions from:
- Michel Reniers (TU/e) et al on the CPSoS project in the special theme section: ‘Core Research and Innovation Areas in Cyber-Physical Systems of Systems’
- Stijn de Gouw and Frank de Boer (CWI) in the R&I section: 'Fixing the Sorting Algorithm for Android, Java and Python'
- In brief news item: Start of Lightning Explained: Hail and Cosmic Particles
Keynote by Werner Steinhögl, Programme Officer at the European Commission, Components and Systems, Directorate General CONNECT: "Trustworthy Systems of Systems – A Prerequisite for the Digitalization of Industry"
http://ercim-news.ercim.eu/en102/keynote
Invited contribution by Andreas Wild, Executive Director of the ECSEL Joint Undertaking: "ECSEL JU Launches Research and Innovation Actions Strengthening European Competitiveness"
http://ercim-news.ercim.eu/en102/special/ecsel-ju-launches-research-and-innovation-actions-strengthening-european-competitiveness
This issue is also available for download in pdf and ebpub
Next issue: No. 103, October 2015 - Special Theme: "Augmented Reality"
(see Call for articles at http://ercim-news.ercim.eu/call)
by Stijn de Gouw and Frank de Boer
In 2013, whilst trying to prove the correctness of TimSort - a broadly applied sorting algorithm - the CWI Formal Methods Group, in collaboration with SDL, Leiden University and TU Darmstadt, instead identified an error in it, which could crash programs and threaten security. Our bug report with an improved version, developed in February 2015, has led to corrected versions in major programming languages and frameworks.
Tim Peters developed the Timsort hybrid sorting algorithm in 2002. TimSort was first developed for Python, a popular programming language, but later ported to Java (where it appears as java.util.Collections.sort and java.util.Arrays.sort). TimSort is today used as the default sorting algorithm in Java, in Android (a widely used platform by Google for mobile devices), in Python and many other programming languages and frameworks. 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.
(…)
So far, this was one of the hardest correctness proofs ever of an existing Java library. It required more than two million rules of inference and thousands of manual steps. With such an widely used language like Java, it is important that software does not crash. This result illustrates the relevance of formal methods, e.g., in Python our fix was quickly applied.
Other recent successful applications of formal methods are INFER, an automatic, separation-logic-based memory safety checker used in Facebook and the Temporal Logic of Actions (TLA). TLA is developed by Leslie Lamport, Recipient of the Turing Award 2013. It is in use by engineers at Amazon Web Services.The work was co-funded by the EU project Envisage.
Link:
http://envisage-project.eu/wp-content/uploads/2015/02/sorting.pdf
