Introduction

Abstract

The development of information processing systems, especially if these consist of concurrent processes, is a very complicated task. In fact, modern computer systems are the most complicated structures mankind has ever built in its history: Modern microprocessors are implemented by millions of transistors; operating systems and software applications consist of millions of lines of code. Therefore, it is no wonder that these systems often have errors that lead to serious malfunctions, even if the systems have been extensively tested to validate their correctness.

Quo facto, quando orientur controversiae, non magis disputatione opus erit inter duos philosophos, quam inter duos computistas. Sufficiet enim calamos in manus sumere sedereque ad abacos, et sibi mutuo (accito si placet amico) dicere: calculemus^l.

— Gottfried Wilhelm Leibniz (1646–1716)