Abstract
Abstract:
Software is in all mission-critical and safety-critical industrial infrastructures since it is, in principle, the cheapest and most effective way to control complex systems in real time. However, all computer scientists have experienced costly bugs in embedded software. The failure of the Ariane 5.01 maiden flight (due to an overflow), the failure of the Patriot missile during the Gulf war (due to an accumulated rounding error), the loss of Mars orbiter (due to a unit error) are a few examples showing that mission-critical and safety-critical software can be far from being safe. Every computer scientist agrees on the fact that it is preferable to verify that missioncritical or safety critical software (and nowadays hardware) programs do not go wrong before running them. As an alternative to testing, which hardly scales up at reasonable costs and with a satisfactory coverage, formal verification has emerged, this last decade, as a promising useful complement, with interesting potential industrial applications.