Finding bugs in computer programs is a daunting task with a curious history. One of the fathers of the technique of model checking (model verification) for the analysis and detection of these failures was Professor Edmund E. Clarke, who died of covid last December. But the research team he led must have shared the glory with the one led in France by Joseph Siffakis because both groups reached similar results simultaneously. A coincidence that is explained by the fact that in those years there was no internet and access to articles from conferences and magazines was delayed in time. In a solomonic way, the 2002 Turing Prize (the equivalent of the Nobel Prize in Informatics) was awarded to both teams for their work on the aforementioned model verification.
Although in recent years, a large part of computer programs that we use in our devices is made up of components that are known to work well, there are others that have to be written manually, because they are specific to the application we are making or because they require human intelligence and cannot be automated.
The complexity of software causes it to contain errors, this is a fact. It has been quantified that for every 1000 lines of code there is on average one wrong line, or if we have already made a great effort to analyze the code, the proportion can reach one error for every 10 000 lines of code.
To imagine the enormity of the task of looking for errors in a huge code, we can think of a large olive tree. It has a solid trunk, which represents the structure on which the software is supported, but then it has many branches, each of which has other smaller branches that can also branch again and again until we find the fruits, the olives. Suppose we want to search for all the olives that, for some reason, are defective, or even worse, imagine that some could be poisoned and it is vital to find them. We could use a brute force procedure, go twig by twig looking for defective or poisonous olives, but this method would be very tedious and time consuming. We could also take a look at the tree to see if, by chance, we see any bad olives. But this method does not convince us either, because, if we do not find any, we cannot be sure that the tree is healthy.
The task of finding a bug in a software complex resembles the search for the poisoned olive. During its execution, the software travels paths that are like branches in the tree. But, a priori, we cannot know which path will be selected. For this reason, we can imagine the impact that, in the 80s, the discovery of automatic methods to track all the branches of the tree efficiently. Unsurprisingly, both Clarke’s and Siffakis They were based on the work of researchers who preceded, such as Zohar Manna and Amir Pnueli, who defined temporal logic in the 70s. This logic allows us to describe the error to look for (the poisoned olive) and, at the same time, helps to the model verification algorithms to perform the search efficiently, pruning (symbolically) those branches in which it is already known that there are no bad olives, which greatly speeds up the search.
Maria del Mar Gallardo Melgarejo She is a professor in the area of Computer Languages and Systems of the Department of Computer Languages and Sciences of the ETSI computer science of the University of Malaga.
Chronicles of the Intangible is a space for the dissemination of computer science, coordinated by the academic society SISTEDES (Society for Software Engineering and Software Development Technologies). The intangible is the non-material part of computer systems (that is, software), and its history and its evolution are related here. The authors are professors from Spanish universities, coordinated by Ricardo Peña Marí (professor at the Complutense University of Madrid) and Macario Polo Usaola (professor at the University of Castilla-La Mancha).
#man #devised #detect #poisoned #olives #computer #programs