

Program Correctness: It's Just a Game Henrik Björklund Making sure that computers and their programs work as they are supposed to is becoming more and more important, as we rely on them in an increasing number of situations. Todays systems are too large to make it possible for a programmer to check his programs manually. This is why we need ways to automatically determine if a system really does what it should. I study this problem through a type of games, played between two players. The first one tries to prove that the program is correct, while the second one tries to find a flaw. If we can find a quick way of figuring out who should win these games, we would at the same time be able to check computer programs quickly. I deal with methods for finding the winner. I work in a small research group at the ITdepartment in Uppsala. We use games to study how computer programs can be checked for their correctness. This is important for software that controls parts of machines for which safety is critical, like airplanes, power plants, cars, and medical equipment. I do not actually write programs for doing automated testing. Rather, the games are a method my group uses in order to investigates how such programs should work. In the games I study, like in many games we play for fun or profit, e.g., chess, go, or poker, a good strategy is needed in order to win. In chess you would ideally like to have a strategy that covers all possible positions on the board, and always tells you which move is optimal. Naturally, strategies can be good or bad. A really good strategy, one that lets you win no matter how your opponent plays, is simply called winning. In a twoplayer game, only one player can have a winning strategy. The problem is how to find out who does. In most games, each player has too many possible strategies to allow us to investigate each one of them. So we need a clever way of searching for a winning strategy without looking at them all. Luckily, for some of the games I work with, there are methods for computing a numerical value for a strategy. The better the strategy, the higher the value. If we find the strategy available to the first player that has the biggest value, it is actually easy to check whether it is winning or not. If it is, we know the player can win, and if not, we know that against all his strategies, the second player has some way of winning. One of the things I have been studying is how we can efficiently find the best value. It turns out that similar strategies most often also have similar values. In other words, the values are not just randomly spread out among the strategies. There is some kind of structure here that might help us in the search. If two strategies are similar, what exactly do their values tell us about the values of other similar strategies? My group has been trying to describe these relationships as thoroughly as possible. For two different game types that I have been working with, the methods for assigning values to strategies actually share some important properties. Surprisingly, it turned out that this method also makes it possible to translate the task of finding the best strategy into a problem that has been intensively studied in a completely different area of computer science. This is good news, since it allows reuse of known methods from that field. It also provides a simpler description of some of the problems in my field. In other words, this research deals with reducing a number of different problems, with different characteristics, into one single, more general problem, that is easier to analyze. One of the things I am doing now is therefore to investigate more game types that are interesting for checking computer programs, to see if they can be described in this simpler way. It is of course also very interesting to try to find new methods for solving the more general problem. It is still not known whether it can be solved fast enough to make it practically useful. My hope that my contributions, together with those of others, will eventually lead to better quality computer software, and a situation where we can rely on it with greater confidence.


Modified 15 January 2003 * Contact Us 