Flawless software: That is the goal of three young CWI researchers who defended their PhD theses on formal methods in October and November 2004. Verification and model checking techniques can automatically check each of the many states that a computer system can be in. In this way, they will detect every error. This is important for safety critical systems, such as the control of helicopters, nuclear reactors or lift systems.
Natalia Ioustinova studied how billions of states in a time-dependent system can be reduced to a smaller number, or even from an infinite to a finite number. Simona Orzan made it possible to distribute the calculations to a network of computers. She tested this at the Linux supercomputercluster at CWI. Bigger problems could be solved in less time. Jun Pang investigated if the theory of formal verification of distributed systems could be applied to industrial engineering processes. In case studies, he looked at both communication protocols and algorithms, for instance for a lift system for trucks. With the new method, better solutions were found. The theses were defended at the Vrije Universiteit in Amsterdam.
